docs(algebra/*): Add docstrings to additive lemmas (#12578)

Many additive lemmas had no docstrings while their multiplicative counterparts had. This adds them in all files under `algebra`.

src/algebra/big_operators/basic.lean

@@ -766,13 +766,15 @@ end
   (∏ x in s, (ite (a = x) (b x) 1)) = ite (a ∈ s) (b a) 1 :=
 prod_dite_eq s a (λ x _, b x)
 
-/--
-  When a product is taken over a conditional whose condition is an equality test on the index
-  and whose alternative is 1, then the product's value is either the term at that index or `1`.
+/-- A product taken over a conditional whose condition is an equality test on the index and whose
+alternative is `1` has value either the term at that index or `1`.
 
-  The difference with `prod_ite_eq` is that the arguments to `eq` are swapped.
--/
-@[simp, to_additive] lemma prod_ite_eq' [decidable_eq α] (s : finset α) (a : α) (b : α → β) :
+The difference with `finset.prod_ite_eq` is that the arguments to `eq` are swapped. -/
+@[simp, to_additive "A sum taken over a conditional whose condition is an equality test on the index
+and whose alternative is `0` has value either the term at that index or `0`.
+
+The difference with `finset.sum_ite_eq` is that the arguments to `eq` are swapped."]
+lemma prod_ite_eq' [decidable_eq α] (s : finset α) (a : α) (b : α → β) :
   (∏ x in s, (ite (x = a) (b x) 1)) = ite (a ∈ s) (b a) 1 :=
 prod_dite_eq' s a (λ x _, b x)
 
@@ -991,7 +993,7 @@ lemma sum_range_induction {M : Type*} [add_comm_monoid M]
   ∑ k in finset.range n, f k = s n :=
 @prod_range_induction (multiplicative M) _ f s h0 h n
 
-/-- A telescoping sum along `{0, ..., n-1}` of an additive commutative group valued function
+/-- A telescoping sum along `{0, ..., n - 1}` of an additive commutative group valued function
 reduces to the difference of the last and first terms.-/
 lemma sum_range_sub {G : Type*} [add_comm_group G] (f : ℕ → G) (n : ℕ) :
   ∑ i in range n, (f (i+1) - f i) = f n - f 0 :=
@@ -1001,16 +1003,16 @@ lemma sum_range_sub' {G : Type*} [add_comm_group G] (f : ℕ → G) (n : ℕ) :
   ∑ i in range n, (f i - f (i+1)) = f 0 - f n :=
 by { apply sum_range_induction; simp }
 
-/-- A telescoping product along `{0, ..., n-1}` of a commutative group valued function
-reduces to the ratio of the last and first factors.-/
+/-- A telescoping product along `{0, ..., n - 1}` of a commutative group valued function reduces to
+the ratio of the last and first factors. -/
 @[to_additive]
 lemma prod_range_div {M : Type*} [comm_group M] (f : ℕ → M) (n : ℕ) :
   ∏ i in range n, (f (i+1) * (f i)⁻¹) = f n * (f 0)⁻¹ :=
 by simpa only [← div_eq_mul_inv] using @sum_range_sub (additive M) _ f n
 
 @[to_additive]
 lemma prod_range_div' {M : Type*} [comm_group M] (f : ℕ → M) (n : ℕ) :
-  ∏ i in range n, (f i * (f (i+1))⁻¹) = (f 0) * (f n)⁻¹ :=
+  ∏ i in range n, (f i * (f (i+1))⁻¹) = f 0 * (f n)⁻¹ :=
 by simpa only [← div_eq_mul_inv] using @sum_range_sub' (additive M) _ f n
 
 /--
@@ -1092,9 +1094,10 @@ finset.strong_induction_on s
         prod_insert (not_mem_erase _ _), ih', mul_one, h x hx]))
 
 
-/-- The product of the composition of functions `f` and `g`, is the product
-over `b ∈ s.image g` of `f b` to the power of the cardinality of the fibre of `b`. See also
-`finset.prod_image`. -/
+/-- The product of the composition of functions `f` and `g`, is the product over `b ∈ s.image g` of
+`f b` to the power of the cardinality of the fibre of `b`. See also `finset.prod_image`. -/
+@[to_additive "The sum of the composition of functions `f` and `g`, is the sum over `b ∈ s.image g`
+of `f b` times of the cardinality of the fibre of `b`. See also `finset.sum_image`."]
 lemma prod_comp [decidable_eq γ] (f : γ → β) (g : α → γ) :
   ∏ a in s, f (g a) = ∏ b in s.image g, f b ^ (s.filter (λ a, g a = b)).card  :=
 calc ∏ a in s, f (g a)
@@ -1291,13 +1294,6 @@ lemma sum_boole {s : finset α} {p : α → Prop} [non_assoc_semiring β] {hp :
   (∑ x in s, if p x then (1 : β) else (0 : β)) = (s.filter p).card :=
 by simp [sum_ite]
 
-lemma sum_comp [add_comm_monoid β] [decidable_eq γ] (f : γ → β) (g : α → γ) :
-  ∑ a in s, f (g a) = ∑ b in s.image g, (s.filter (λ a, g a = b)).card • (f b) :=
-@prod_comp (multiplicative β) _ _ _ _ _ _ _
-attribute [to_additive "The sum of the composition of functions `f` and `g`, is the sum
-over `b ∈ s.image g` of `f b` times of the cardinality of the fibre of `b`. See also
-`finset.sum_image`."] prod_comp
-
 lemma eq_sum_range_sub [add_comm_group β] (f : ℕ → β) (n : ℕ) :
   f n = f 0 + ∑ i in range n, (f (i+1) - f i) :=
 by rw [finset.sum_range_sub, add_sub_cancel'_right]

src/algebra/big_operators/nat_antidiagonal.lean

@@ -64,7 +64,8 @@ end
 
 /-- This lemma matches more generally than `finset.nat.prod_antidiagonal_eq_prod_range_succ_mk` when
 using `rw ←`. -/
-@[to_additive]
+@[to_additive "This lemma matches more generally than
+`finset.nat.sum_antidiagonal_eq_sum_range_succ_mk` when using `rw ←`."]
 lemma prod_antidiagonal_eq_prod_range_succ {M : Type*} [comm_monoid M] (f : ℕ → ℕ → M) (n : ℕ) :
   ∏ ij in finset.nat.antidiagonal n, f ij.1 ij.2 = ∏ k in range n.succ, f k (n - k) :=
 prod_antidiagonal_eq_prod_range_succ_mk _ _

src/algebra/big_operators/ring.lean

@@ -218,7 +218,8 @@ end comm_ring
 
 /-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
 of `s`, and over all subsets of `s` to which one adds `x`. -/
-@[to_additive]
+@[to_additive "A sum over all subsets of `s ∪ {x}` is obtained by summing the sum over all subsets
+of `s`, and over all subsets of `s` to which one adds `x`."]
 lemma prod_powerset_insert [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x ∉ s)
   (f : finset α → β) :
   (∏ a in (insert x s).powerset, f a) =
@@ -235,9 +236,10 @@ begin
     exact ne_insert_of_not_mem _ _ (not_mem_of_mem_powerset_of_not_mem h₁ h) }
 end
 
-/-- A product over `powerset s` is equal to the double product over
-sets of subsets of `s` with `card s = k`, for `k = 1, ... , card s`. -/
-@[to_additive]
+/-- A product over `powerset s` is equal to the double product over sets of subsets of `s` with
+`card s = k`, for `k = 1, ..., card s`. -/
+@[to_additive "A sum over `powerset s` is equal to the double sum over sets of subsets of `s` with
+`card s = k`, for `k = 1, ..., card s`"]
 lemma prod_powerset [comm_monoid β] (s : finset α) (f : finset α → β) :
   ∏ t in powerset s, f t = ∏ j in range (card s + 1), ∏ t in powerset_len j s, f t :=
 begin

src/algebra/category/Group/limits.lean

@@ -58,13 +58,14 @@ begin
   apply_instance,
 end
 
-/--
-We show that the forgetful functor `Group ⥤ Mon` creates limits.
+/-- We show that the forgetful functor `Group ⥤ Mon` creates limits.
 
-All we need to do is notice that the limit point has a `group` instance available,
-and then reuse the existing limit.
--/
-@[to_additive]
+All we need to do is notice that the limit point has a `group` instance available, and then reuse
+the existing limit. -/
+@[to_additive "We show that the forgetful functor `AddGroup ⥤ AddMon` creates limits.
+
+All we need to do is notice that the limit point has an `add_group` instance available, and then
+reuse the existing limit."]
 instance (F : J ⥤ Group) : creates_limit F (forget₂ Group Mon.{u}) :=
 creates_limit_of_reflects_iso (λ c' t,
 { lifted_cone :=
@@ -95,26 +96,30 @@ def limit_cone_is_limit (F : J ⥤ Group) : is_limit (limit_cone F) :=
 lifted_limit_is_limit _
 
 /-- The category of groups has all limits. -/
-@[to_additive]
+@[to_additive "The category of additive groups has all limits."]
 instance has_limits : has_limits Group :=
 { has_limits_of_shape := λ J 𝒥, by exactI
   { has_limit := λ F, has_limit_of_created F (forget₂ Group Mon) } } -- TODO use the above instead?
 
-/--
-The forgetful functor from groups to monoids preserves all limits.
-(That is, the underlying monoid could have been computed instead as limits in the category
-of monoids.)
+/-- The forgetful functor from groups to monoids preserves all limits.
+
+This means the underlying monoid of a limit can be computed as a limit in the category of monoids.
 -/
-@[to_additive AddGroup.forget₂_AddMon_preserves_limits]
+@[to_additive AddGroup.forget₂_AddMon_preserves_limits "The forgetful functor from additive groups
+to additive monoids preserves all limits.
+
+This means the underlying additive monoid of a limit can be computed as a limit in the category of
+additive monoids."]
 instance forget₂_Mon_preserves_limits : preserves_limits (forget₂ Group Mon) :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ F, by apply_instance } }
 
-/--
-The forgetful functor from groups to types preserves all limits. (That is, the underlying
-types could have been computed instead as limits in the category of types.)
--/
-@[to_additive]
+/-- The forgetful functor from groups to types preserves all limits.
+
+This means the underlying type of a limit can be computed as a limit in the category of types. -/
+@[to_additive "The forgetful functor from additive groups to types preserves all limits.
+
+This means the underlying type of a limit can be computed as a limit in the category of types."]
 instance forget_preserves_limits : preserves_limits (forget Group) :=
 { preserves_limits_of_shape := λ J 𝒥, by exactI
   { preserves_limit := λ F, limits.comp_preserves_limit (forget₂ Group Mon) (forget Mon) } }

src/algebra/category/Mon/limits.lean

@@ -96,18 +96,19 @@ end has_limits
 open has_limits
 
 /-- The category of monoids has all limits. -/
-@[to_additive]
+@[to_additive "The category of additive monoids has all limits."]
 instance has_limits : has_limits Mon :=
 { has_limits_of_shape := λ J 𝒥, by exactI
   { has_limit := λ F, has_limit.mk
     { cone     := limit_cone F,
       is_limit := limit_cone_is_limit F } } }
 
-/--
-The forgetful functor from monoids to types preserves all limits. (That is, the underlying
-types could have been computed instead as limits in the category of types.)
--/
-@[to_additive]
+/-- The forgetful functor from monoids to types preserves all limits.
+
+This means the underlying type of a limit can be computed as a limit in the category of types. -/
+@[to_additive "The forgetful functor from additive monoids to types preserves all limits.
+
+This means the underlying type of a limit can be computed as a limit in the category of types."]
 instance forget_preserves_limits : preserves_limits (forget Mon) :=
 { preserves_limits_of_shape := λ J 𝒥, by exactI
   { preserves_limit := λ F, preserves_limit_of_preserves_limit_cone
@@ -130,13 +131,14 @@ instance limit_comm_monoid (F : J ⥤ CommMon) :
 @submonoid.to_comm_monoid (Π j, F.obj j) _
   (Mon.sections_submonoid (F ⋙ forget₂ CommMon Mon.{u}))
 
-/--
-We show that the forgetful functor `CommMon ⥤ Mon` creates limits.
+/-- We show that the forgetful functor `CommMon ⥤ Mon` creates limits.
 
 All we need to do is notice that the limit point has a `comm_monoid` instance available,
-and then reuse the existing limit.
--/
-@[to_additive]
+and then reuse the existing limit. -/
+@[to_additive "We show that the forgetful functor `AddCommMon ⥤ AddMon` creates limits.
+
+All we need to do is notice that the limit point has an `add_comm_monoid` instance available,
+and then reuse the existing limit."]
 instance (F : J ⥤ CommMon) : creates_limit F (forget₂ CommMon Mon.{u}) :=
 creates_limit_of_reflects_iso (λ c' t,
 { lifted_cone :=
@@ -167,26 +169,30 @@ def limit_cone_is_limit (F : J ⥤ CommMon) : is_limit (limit_cone F) :=
 lifted_limit_is_limit _
 
 /-- The category of commutative monoids has all limits. -/
-@[to_additive]
+@[to_additive "The category of commutative monoids has all limits."]
 instance has_limits : has_limits CommMon :=
 { has_limits_of_shape := λ J 𝒥, by exactI
   { has_limit := λ F, has_limit_of_created F (forget₂ CommMon Mon) } }
 
-/--
-The forgetful functor from commutative monoids to monoids preserves all limits.
-(That is, the underlying monoid could have been computed instead as limits in the category
-of monoids.)
--/
-@[to_additive AddCommMon.forget₂_AddMon_preserves_limits]
+/-- The forgetful functor from commutative monoids to monoids preserves all limits.
+
+This means the underlying type of a limit can be computed as a limit in the category of monoids. -/
+@[to_additive AddCommMon.forget₂_AddMon_preserves_limits "The forgetful functor from additive
+commutative monoids to additive monoids preserves all limits.
+
+This means the underlying type of a limit can be computed as a limit in the category of additive
+monoids."]
 instance forget₂_Mon_preserves_limits : preserves_limits (forget₂ CommMon Mon) :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ F, by apply_instance } }
 
-/--
-The forgetful functor from commutative monoids to types preserves all limits. (That is, the
-underlying types could have been computed instead as limits in the category of types.)
--/
-@[to_additive]
+/-- The forgetful functor from commutative monoids to types preserves all limits.
+
+This means the underlying type of a limit can be computed as a limit in the category of types. -/
+@[to_additive "The forgetful functor from additive commutative monoids to types preserves all
+limits.
+
+This means the underlying type of a limit can be computed as a limit in the category of types."]
 instance forget_preserves_limits : preserves_limits (forget CommMon) :=
 { preserves_limits_of_shape := λ J 𝒥, by exactI
   { preserves_limit := λ F, limits.comp_preserves_limit (forget₂ CommMon Mon) (forget Mon) } }

src/algebra/group/commute.lean

@@ -35,14 +35,16 @@ section has_mul
 variables {S : Type*} [has_mul S]
 
 /-- Equality behind `commute a b`; useful for rewriting. -/
-@[to_additive] protected theorem eq {a b : S} (h : commute a b) : a * b = b * a := h
+@[to_additive "Equality behind `add_commute a b`; useful for rewriting."]
+protected lemma eq {a b : S} (h : commute a b) : a * b = b * a := h
 
 /-- Any element commutes with itself. -/
-@[refl, simp, to_additive] protected theorem refl (a : S) : commute a a := eq.refl (a * a)
+@[refl, simp, to_additive "Any element commutes with itself."]
+protected lemma refl (a : S) : commute a a := eq.refl (a * a)
 
 /-- If `a` commutes with `b`, then `b` commutes with `a`. -/
-@[symm, to_additive] protected theorem symm {a b : S} (h : commute a b) : commute b a :=
-eq.symm h
+@[symm, to_additive "If `a` commutes with `b`, then `b` commutes with `a`."]
+protected lemma symm {a b : S} (h : commute a b) : commute b a := eq.symm h
 
 @[to_additive] protected theorem semiconj_by {a b : S} (h : commute a b) : semiconj_by a b b := h
 
@@ -57,14 +59,12 @@ section semigroup
 variables {S : Type*} [semigroup S] {a b c : S}
 
 /-- If `a` commutes with both `b` and `c`, then it commutes with their product. -/
-@[simp, to_additive] theorem mul_right (hab : commute a b) (hac : commute a c) :
-  commute a (b * c) :=
-hab.mul_right hac
+@[simp, to_additive "If `a` commutes with both `b` and `c`, then it commutes with their sum."]
+lemma mul_right (hab : commute a b) (hac : commute a c) : commute a (b * c) := hab.mul_right hac
 
 /-- If both `a` and `b` commute with `c`, then their product commutes with `c`. -/
-@[simp, to_additive] theorem mul_left (hac : commute a c) (hbc : commute b c) :
-  commute (a * b) c :=
-hac.mul_left hbc
+@[simp, to_additive "If both `a` and `b` commute with `c`, then their product commutes with `c`."]
+lemma mul_left (hac : commute a c) (hbc : commute b c) : commute (a * b) c := hac.mul_left hbc
 
 @[to_additive] protected lemma right_comm (h : commute b c) (a : S) :
   a * b * c = a * c * b :=

src/algebra/group/freiman.lean

@@ -79,7 +79,9 @@ class add_freiman_hom_class (F : Type*) (A : out_param $ set α) (β : out_param
 
 /-- `freiman_hom_class F A β n` states that `F` is a type of `n`-ary products-preserving morphisms.
 You should extend this class when you extend `freiman_hom`. -/
-@[to_additive add_freiman_hom_class]
+@[to_additive add_freiman_hom_class
+"`add_freiman_hom_class F A β n` states that `F` is a type of `n`-ary sums-preserving morphisms.
+You should extend this class when you extend `add_freiman_hom`."]
 class freiman_hom_class (F : Type*) (A : out_param $ set α) (β : out_param $ Type*) [comm_monoid α]
   [comm_monoid β] (n : ℕ) [fun_like F α (λ _, β)] :=
 (map_prod_eq_map_prod' (f : F) {s t : multiset α} (hsA : ∀ ⦃x⦄, x ∈ s → x ∈ A)
@@ -216,7 +218,8 @@ instance : has_mul (A →*[n] β) :=
 
 /-- If `f` is a Freiman homomorphism to a commutative group, then `f⁻¹` is the Freiman homomorphism
 sending `x` to `(f x)⁻¹`. -/
-@[to_additive]
+@[to_additive "If `f` is a Freiman homomorphism to an additive commutative group, then `-f` is the
+Freiman homomorphism sending `x` to `-f x`."]
 instance : has_inv (A →*[n] G) :=
 ⟨λ f, { to_fun := λ x, (f x)⁻¹,
   map_prod_eq_map_prod' := λ s t hsA htA hs ht h,
@@ -288,7 +291,11 @@ end freiman_hom
 
 We can't leave the domain `A : set α` of the `freiman_hom` a free variable, since it wouldn't be
 inferrable. -/
-@[to_additive]
+@[to_additive " An additive monoid homomorphism is naturally an `add_freiman_hom` on its entire
+domain.
+
+We can't leave the domain `A : set α` of the `freiman_hom` a free variable, since it wouldn't be
+inferrable."]
 instance monoid_hom.freiman_hom_class : freiman_hom_class (α →* β) set.univ β n :=
 { map_prod_eq_map_prod' := λ f s t _ _ _ _ h, by rw [←f.map_multiset_prod, h, f.map_multiset_prod] }