From d67062f407fb34426d7ad70fd1e3b108fb37ab2d Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 7 Oct 2020 21:39:17 +0000
Subject: [PATCH] chore(algebra/pointwise): add `###` here and there (#4514)

---
 src/algebra/pointwise.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean
index 9ba9673a888c0..37bc8594eb116 100644
--- a/src/algebra/pointwise.lean
+++ b/src/algebra/pointwise.lean
@@ -40,7 +40,7 @@ open function
 
 variables {α : Type*} {β : Type*} {s s₁ s₂ t t₁ t₂ u : set α} {a b : α} {x y : β}
 
-/-! Properties about 1 -/
+/-! ### Properties about 1 -/
 @[to_additive]
 instance [has_one α] : has_one (set α) := ⟨{1}⟩
 
@@ -62,7 +62,8 @@ theorem one_nonempty [has_one α] : (1 : set α).nonempty := ⟨1, rfl⟩
 @[simp, to_additive]
 theorem image_one [has_one α] {f : α → β} : f '' 1 = {f 1} := image_singleton
 
-/-! Properties about multiplication -/
+/-! ### Properties about multiplication -/
+
 @[to_additive]
 instance [has_mul α] : has_mul (set α) := ⟨image2 has_mul.mul⟩
 
@@ -189,7 +190,7 @@ def fintype_mul [has_mul α] [decidable_eq α] (s t : set α) [hs : fintype s] [
   fintype (s * t : set α) :=
 set.fintype_image2 _ s t
 
-/-! Properties about inversion -/
+/-! ### Properties about inversion -/
 @[to_additive set.has_neg'] -- todo: remove prime once name becomes available
 instance [has_inv α] : has_inv (set α) :=
 ⟨preimage has_inv.inv⟩
@@ -231,7 +232,7 @@ lemma inv_subset_inv [group α] {s t : set α} : s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t :
 @[to_additive] lemma inv_subset [group α] {s t : set α} : s⁻¹ ⊆ t ↔ s ⊆ t⁻¹ :=
 by { rw [← inv_subset_inv, set.inv_inv] }
 
-/-! Properties about scalar multiplication -/
+/-! ### Properties about scalar multiplication -/
 
 /-- Scaling a set: multiplying every element by a scalar. -/
 instance has_scalar_set [has_scalar α β] : has_scalar α (set β) :=
@@ -279,7 +280,7 @@ image2_singleton_left
 
 section monoid
 
-/-! `set α` as a `(∪,*)`-semiring -/
+/-! ### `set α` as a `(∪,*)`-semiring -/
 
 /-- An alias for `set α`, which has a semiring structure given by `∪` as "addition" and pointwise
   multiplication `*` as "multiplication". -/