chore(Algebra/BigOperators): add missing deprecation dates (#12597)

One additivised lemma was missing a deprecation.
leanprover-community · May 24, 2024 · 0c2aeec · 0c2aeec
1 parent 9db13e9
commit 0c2aeec
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 8 deletions.
diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean
@@ -240,7 +240,7 @@ theorem map_finsupp_prod [Zero M] [CommMonoid N] [CommMonoid P] {H : Type*}
 #align map_finsupp_sum map_finsupp_sum
 
 /-- Deprecated, use `_root_.map_finsupp_prod` instead. -/
-@[to_additive (attr := deprecated)
+@[to_additive (attr := deprecated (since := "2021-12-30"))
   "Deprecated, use `_root_.map_finsupp_sum` instead."]
 protected theorem MulEquiv.map_finsupp_prod [Zero M] [CommMonoid N] [CommMonoid P] (h : N ≃* P)
     (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod fun a b => h (g a b) :=
@@ -249,7 +249,7 @@ protected theorem MulEquiv.map_finsupp_prod [Zero M] [CommMonoid N] [CommMonoid
 #align add_equiv.map_finsupp_sum AddEquiv.map_finsupp_sum
 
 /-- Deprecated, use `_root_.map_finsupp_prod` instead. -/
-@[to_additive (attr := deprecated)
+@[to_additive (attr := deprecated (since := "2021-12-30"))
   "Deprecated, use `_root_.map_finsupp_sum` instead."]
 protected theorem MonoidHom.map_finsupp_prod [Zero M] [CommMonoid N] [CommMonoid P] (h : N →* P)
     (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod fun a b => h (g a b) :=
@@ -258,14 +258,14 @@ protected theorem MonoidHom.map_finsupp_prod [Zero M] [CommMonoid N] [CommMonoid
 #align add_monoid_hom.map_finsupp_sum AddMonoidHom.map_finsupp_sum
 
 /-- Deprecated, use `_root_.map_finsupp_sum` instead. -/
-@[deprecated map_finsupp_sum]
+@[deprecated map_finsupp_sum (since := "2021-12-30")]
 protected theorem RingHom.map_finsupp_sum [Zero M] [Semiring R] [Semiring S] (h : R →+* S)
     (f : α →₀ M) (g : α → M → R) : h (f.sum g) = f.sum fun a b => h (g a b) :=
   map_finsupp_sum h f g
 #align ring_hom.map_finsupp_sum RingHom.map_finsupp_sum
 
 /-- Deprecated, use `_root_.map_finsupp_prod` instead. -/
-@[deprecated map_finsupp_prod]
+@[deprecated map_finsupp_prod (since := "2021-12-30")]
 protected theorem RingHom.map_finsupp_prod [Zero M] [CommSemiring R] [CommSemiring S] (h : R →+* S)
     (f : α →₀ M) (g : α → M → R) : h (f.prod g) = f.prod fun a b => h (g a b) :=
   map_finsupp_prod h f g

diff --git a/Mathlib/Algebra/BigOperators/Group/List.lean b/Mathlib/Algebra/BigOperators/Group/List.lean
@@ -690,8 +690,9 @@ theorem map_list_prod {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F)
 
 namespace MonoidHom
 
+-- original lemma deprecated on 2023-01-10; additivised lemma on 2024-05-02
 /-- Deprecated, use `_root_.map_list_prod` instead. -/
-@[to_additive "Deprecated, use `_root_.map_list_sum` instead."]
+@[to_additive (attr := deprecated) "Deprecated, use `_root_.map_list_sum` instead."]
 protected theorem map_list_prod (f : M →* N) (l : List M) : f l.prod = (l.map f).prod :=
   map_list_prod f l
 #align monoid_hom.map_list_prod MonoidHom.map_list_prod

diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
@@ -211,7 +211,7 @@ noncomputable def expMonoidHom : MonoidHom (Multiplicative ℂ) ℂ :=
     map_mul' := by simp [exp_add] }
 
 theorem exp_list_sum (l : List ℂ) : exp l.sum = (l.map exp).prod :=
-  @MonoidHom.map_list_prod (Multiplicative ℂ) ℂ _ _ expMonoidHom l
+  map_list_prod (M := Multiplicative ℂ) expMonoidHom l
 #align complex.exp_list_sum Complex.exp_list_sum
 
 theorem exp_multiset_sum (s : Multiset ℂ) : exp s.sum = (s.map exp).prod :=
@@ -832,7 +832,7 @@ noncomputable def expMonoidHom : MonoidHom (Multiplicative ℝ) ℝ :=
     map_mul' := by simp [exp_add] }
 
 theorem exp_list_sum (l : List ℝ) : exp l.sum = (l.map exp).prod :=
-  @MonoidHom.map_list_prod (Multiplicative ℝ) ℝ _ _ expMonoidHom l
+  map_list_prod (M := Multiplicative ℝ) expMonoidHom l
 #align real.exp_list_sum Real.exp_list_sum
 
 theorem exp_multiset_sum (s : Multiset ℝ) : exp s.sum = (s.map exp).prod :=

diff --git a/Mathlib/GroupTheory/Coxeter/Length.lean b/Mathlib/GroupTheory/Coxeter/Length.lean
@@ -131,7 +131,7 @@ theorem lengthParity_comp_simple :
 theorem lengthParity_eq_ofAdd_length (w : W) :
     cs.lengthParity w = Multiplicative.ofAdd (↑(ℓ w)) := by
   rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
-  rw [← hω, wordProd, MonoidHom.map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
+  rw [← hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
     prod_replicate, ← ofAdd_nsmul, nsmul_one]
 
 theorem length_mul_mod_two (w₁ w₂ : W) : ℓ (w₁ * w₂) % 2 = (ℓ w₁ + ℓ w₂) % 2 := by