From 693e49b9f4c1a1c5ef12f7abd6c0ab50558f4e39 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Thu, 26 Oct 2023 13:41:30 +0200 Subject: [PATCH] chore: typos in to_addive docs --- Mathlib/Algebra/BigOperators/Basic.lean | 2 +- Mathlib/Algebra/BigOperators/Finprod.lean | 2 +- Mathlib/Algebra/Group/Prod.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index 2632d094c0976..16ecbd79f7c96 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -683,7 +683,7 @@ theorem prod_product_right {s : Finset γ} {t : Finset α} {f : γ × α → β} #align finset.sum_product_right Finset.sum_product_right /-- An uncurried version of `Finset.prod_product_right`. -/ -@[to_additive "An uncurried version of `Finset.prod_product_right`"] +@[to_additive "An uncurried version of `Finset.sum_product_right`"] theorem prod_product_right' {s : Finset γ} {t : Finset α} {f : γ → α → β} : ∏ x in s ×ˢ t, f x.1 x.2 = ∏ y in t, ∏ x in s, f x y := prod_product_right diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean index 66cd2ae32d77b..e2f481aab0552 100644 --- a/Mathlib/Algebra/BigOperators/Finprod.lean +++ b/Mathlib/Algebra/BigOperators/Finprod.lean @@ -651,7 +651,7 @@ theorem finprod_mem_mul_distrib' (hf : (s ∩ mulSupport f).Finite) (hg : (s ∩ #align finsum_mem_add_distrib' finsum_mem_add_distrib' /-- The product of the constant function `1` over any set equals `1`. -/ -@[to_additive "The product of the constant function `0` over any set equals `0`."] +@[to_additive "The sum of the constant function `0` over any set equals `0`."] theorem finprod_mem_one (s : Set α) : (∏ᶠ i ∈ s, (1 : M)) = 1 := by simp #align finprod_mem_one finprod_mem_one #align finsum_mem_zero finsum_mem_zero diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean index 1003edceeac13..b49a495663e9a 100644 --- a/Mathlib/Algebra/Group/Prod.lean +++ b/Mathlib/Algebra/Group/Prod.lean @@ -378,7 +378,7 @@ variable {M' : Type*} {N' : Type*} [Mul M] [Mul N] [Mul M'] [Mul N'] [Mul P] (f (g : N →ₙ* N') /-- `Prod.map` as a `MonoidHom`. -/ -@[to_additive prodMap "`prod.map` as an `AddMonoidHom`"] +@[to_additive prodMap "`Prod.map` as an `AddMonoidHom`"] def prodMap : M × N →ₙ* M' × N' := (f.comp (fst M N)).prod (g.comp (snd M N)) #align mul_hom.prod_map MulHom.prodMap