Skip to content

Commit 1cd5402

Browse files
leanprover-community-bot-assistantbryangingechenleanprover-community-mathlib4-botpre-commit-ci-lite[bot]adomani
committed
chore: remove declarations deprecated before 2025-04-21 (#30759)
I am happy to remove some deprecated declarations for you! Please check if there are any remaining stray comments or other issues before merging. The following files contained only deprecated declarations and have been deleted: - Mathlib/Deprecated/AnalyticManifold.lean - Mathlib/Geometry/Manifold/AnalyticManifold.lean Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: adomani <adomani@gmail.com>
1 parent e280942 commit 1cd5402

File tree

385 files changed

+127
-3921
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

385 files changed

+127
-3921
lines changed

‎Mathlib.lean‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3826,7 +3826,6 @@ import Mathlib.Data.ZMod.QuotientRing
38263826
import Mathlib.Data.ZMod.Units
38273827
import Mathlib.Data.ZMod.ValMinAbs
38283828
import Mathlib.Deprecated.Aliases
3829-
import Mathlib.Deprecated.AnalyticManifold
38303829
import Mathlib.Deprecated.Estimator
38313830
import Mathlib.Deprecated.MLList.BestFirst
38323831
import Mathlib.Deprecated.Order
@@ -3976,7 +3975,6 @@ import Mathlib.Geometry.Manifold.Algebra.LieGroup
39763975
import Mathlib.Geometry.Manifold.Algebra.Monoid
39773976
import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
39783977
import Mathlib.Geometry.Manifold.Algebra.Structures
3979-
import Mathlib.Geometry.Manifold.AnalyticManifold
39803978
import Mathlib.Geometry.Manifold.Bordism
39813979
import Mathlib.Geometry.Manifold.BumpFunction
39823980
import Mathlib.Geometry.Manifold.ChartedSpace

‎Mathlib/Algebra/BigOperators/Associated.lean‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -222,12 +222,8 @@ theorem Prime.dvd_finsuppProd_iff {f : M₀ →₀ M} {g : M₀ → M → ℕ} {
222222
p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a) :=
223223
Prime.dvd_finset_prod_iff pp _
224224

225-
@[deprecated (since := "2025-04-06")] alias Prime.dvd_finsupp_prod_iff := Prime.dvd_finsuppProd_iff
226-
227225
theorem Prime.not_dvd_finsuppProd {f : M₀ →₀ M} {g : M₀ → M → ℕ} {p : ℕ} (pp : Prime p)
228226
(hS : ∀ a ∈ f.support, ¬p ∣ g a (f a)) : ¬p ∣ f.prod g :=
229227
Prime.not_dvd_finset_prod pp hS
230228

231-
@[deprecated (since := "2025-04-06")] alias Prime.not_dvd_finsupp_prod := Prime.not_dvd_finsuppProd
232-
233229
end CommMonoidWithZero

‎Mathlib/Algebra/BigOperators/Fin.lean‎

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -85,23 +85,11 @@ theorem prod_univ_castSucc (f : Fin (n + 1) → M) :
8585
theorem prod_univ_getElem (l : List M) : ∏ i : Fin l.length, l[i.1] = l.prod := by
8686
simp [Finset.prod_eq_multiset_prod]
8787

88-
@[deprecated (since := "2025-04-19")]
89-
alias sum_univ_get := sum_univ_getElem
90-
91-
@[to_additive existing, deprecated (since := "2025-04-19")]
92-
alias prod_univ_get := prod_univ_getElem
93-
9488
@[to_additive (attr := simp)]
9589
theorem prod_univ_fun_getElem (l : List ι) (f : ι → M) :
9690
∏ i : Fin l.length, f l[i.1] = (l.map f).prod := by
9791
simp [Finset.prod_eq_multiset_prod]
9892

99-
@[deprecated (since := "2025-04-19")]
100-
alias sum_univ_get' := sum_univ_fun_getElem
101-
102-
@[to_additive existing, deprecated (since := "2025-04-19")]
103-
alias prod_univ_get' := prod_univ_fun_getElem
104-
10593
@[to_additive (attr := simp)]
10694
theorem prod_cons (x : M) (f : Fin n → M) :
10795
(∏ i : Fin n.succ, (cons x f : Fin n.succ → M) i) = x * ∏ i : Fin n, f i := by

‎Mathlib/Algebra/BigOperators/Finsupp/Basic.lean‎

Lines changed: 0 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -163,9 +163,6 @@ theorem _root_.SubmonoidClass.finsuppProd_mem {S : Type*} [SetLike S N] [Submono
163163
(s : S) (f : α →₀ M) (g : α → M → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s :=
164164
prod_mem fun _i hi => h _ (Finsupp.mem_support_iff.mp hi)
165165

166-
@[deprecated (since := "2025-04-06")]
167-
alias _root_.SubmonoidClass.finsupp_prod_mem := _root_.SubmonoidClass.finsuppProd_mem
168-
169166
@[to_additive]
170167
theorem prod_congr {f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) :
171168
f.prod g1 = f.prod g2 :=
@@ -200,28 +197,16 @@ theorem map_finsuppProd [Zero M] [CommMonoid N] [CommMonoid P] {H : Type*}
200197
(h : H) (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod fun a b => h (g a b) :=
201198
map_prod h _ _
202199

203-
@[deprecated (since := "2025-04-06")] alias map_finsupp_prod := map_finsuppProd
204-
@[deprecated (since := "2025-04-06")] alias map_finsupp_sum := map_finsuppSum
205-
206200
@[to_additive]
207201
theorem MonoidHom.coe_finsuppProd [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β)
208202
(g : α → β → N →* P) : ⇑(f.prod g) = f.prod fun i fi => ⇑(g i fi) :=
209203
MonoidHom.coe_finset_prod _ _
210204

211-
@[deprecated (since := "2025-04-06")] alias MonoidHom.coe_finsupp_prod := MonoidHom.coe_finsuppProd
212-
@[deprecated (since := "2025-04-06")]
213-
alias AddMonoidHom.coe_finsupp_sum := AddMonoidHom.coe_finsuppSum
214-
215205
@[to_additive (attr := simp)]
216206
theorem MonoidHom.finsuppProd_apply [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β)
217207
(g : α → β → N →* P) (x : N) : f.prod g x = f.prod fun i fi => g i fi x :=
218208
MonoidHom.finset_prod_apply _ _ _
219209

220-
@[deprecated (since := "2025-04-06")]
221-
alias MonoidHom.finsupp_prod_apply := MonoidHom.finsuppProd_apply
222-
@[deprecated (since := "2025-04-06")]
223-
alias AddMonoidHom.finsupp_sum_apply := AddMonoidHom.finsuppSum_apply
224-
225210
namespace Finsupp
226211

227212
theorem single_multiset_sum [AddCommMonoid M] (s : Multiset M) (a : α) :

‎Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ In this file we prove theorems about products and sums indexed by a `Finset`.
1414
-/
1515

1616
-- TODO: assert_not_exists AddCommMonoidWithOne
17-
assert_not_exists MonoidWithZero MulAction OrderedCommMonoid
17+
assert_not_exists MonoidWithZero MulAction IsOrderedMonoid
1818
assert_not_exists Finset.preimage Finset.sigma Fintype.piFinset
1919
assert_not_exists Finset.piecewise Set.indicator MonoidHom.coeFn Function.support IsSquare
2020

@@ -115,8 +115,6 @@ theorem prod_eq_one (h : ∀ x ∈ s, f x = 1) : ∏ x ∈ s, f x = 1 := calc
115115
lemma prod_eq_one_iff [Subsingleton Mˣ] : ∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1 := by
116116
induction s using Finset.cons_induction <;> simp [*]
117117

118-
@[deprecated (since := "2025-03-31")] alias prod_eq_one_iff' := prod_eq_one_iff
119-
120118
@[to_additive]
121119
theorem prod_disjUnion (h) :
122120
∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x := by

‎Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ See the documentation of `to_additive.attr` for more information.
4444
-- assert_not_exists AddCommMonoidWithOne
4545
assert_not_exists MonoidWithZero
4646
assert_not_exists MulAction
47-
assert_not_exists OrderedCommMonoid
47+
assert_not_exists IsOrderedMonoid
4848

4949
variable {ι κ M N G α : Type*}
5050

@@ -386,9 +386,6 @@ section ToList
386386
theorem prod_map_toList (s : Finset ι) (f : ι → M) : (s.toList.map f).prod = s.prod f := by
387387
rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]
388388

389-
@[deprecated (since := "2025-04-09")] alias prod_to_list := prod_map_toList
390-
@[deprecated (since := "2025-04-09")] alias sum_to_list := sum_map_toList
391-
392389
@[to_additive (attr := simp, grind =)]
393390
theorem prod_toList {M : Type*} [CommMonoid M] (s : Finset M) :
394391
s.toList.prod = ∏ x ∈ s, x := by

‎Mathlib/Algebra/BigOperators/Group/Finset/Pi.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ import Mathlib.Algebra.BigOperators.Group.Finset.Defs
1212
1313
-/
1414

15-
assert_not_exists MonoidWithZero MulAction OrderedCommMonoid
15+
assert_not_exists MonoidWithZero MulAction IsOrderedMonoid
1616

1717
variable {ι β : Type*}
1818

‎Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ import Mathlib.Algebra.BigOperators.Group.Finset.Basic
1010
# Sums and products over preimages of finite sets.
1111
-/
1212

13-
assert_not_exists MonoidWithZero MulAction OrderedCommMonoid
13+
assert_not_exists MonoidWithZero MulAction IsOrderedMonoid
1414

1515
variable {ι κ β : Type*}
1616

‎Mathlib/Algebra/Category/Grp/Basic.lean‎

Lines changed: 0 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -599,31 +599,3 @@ abbrev CommGrpMax.{u1, u2} := CommGrpCat.{max u1 u2}
599599
/-- An alias for `AddCommGrpCat.{max u v}`, to deal around unification issues. -/
600600
@[nolint checkUnivs]
601601
abbrev AddCommGrpMax.{u1, u2} := AddCommGrpCat.{max u1 u2}
602-
603-
/-!
604-
Deprecated lemmas for `MonoidHom.comp` and categorical identities.
605-
-/
606-
607-
@[to_additive (attr := deprecated
608-
"Proven by `simp only [GrpCat.hom_id, comp_id]`"
609-
(since := "2025-01-28"))]
610-
theorem MonoidHom.comp_id_grp {G : GrpCat.{u}} {H : Type u} [Monoid H] (f : G →* H) :
611-
f.comp (GrpCat.Hom.hom (𝟙 G)) = f := by simp
612-
@[to_additive (attr := deprecated
613-
"Proven by `simp only [GrpCat.hom_id, id_comp]`"
614-
(since := "2025-01-28"))]
615-
theorem MonoidHom.id_grp_comp {G : Type u} [Monoid G] {H : GrpCat.{u}} (f : G →* H) :
616-
MonoidHom.comp (GrpCat.Hom.hom (𝟙 H)) f = f := by simp
617-
618-
@[to_additive (attr := deprecated
619-
"Proven by `simp only [CommGrpCat.hom_id, comp_id]`"
620-
(since := "2025-01-28"))]
621-
theorem MonoidHom.comp_id_commGrp {G : CommGrpCat.{u}} {H : Type u} [Monoid H] (f : G →* H) :
622-
f.comp (CommGrpCat.Hom.hom (𝟙 G)) = f := by
623-
simp
624-
@[to_additive (attr := deprecated
625-
"Proven by `simp only [CommGrpCat.hom_id, id_comp]`"
626-
(since := "2025-01-28"))]
627-
theorem MonoidHom.id_commGrp_comp {G : Type u} [Monoid G] {H : CommGrpCat.{u}} (f : G →* H) :
628-
MonoidHom.comp (CommGrpCat.Hom.hom (𝟙 H)) f = f := by
629-
simp

‎Mathlib/Algebra/Category/ModuleCat/Presheaf/Pullback.lean‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -48,9 +48,6 @@ on a certain object `M : PresheafOfModules S`. -/
4848
abbrev pullbackObjIsDefined : ObjectProperty (PresheafOfModules.{v} S) :=
4949
(pushforward φ).leftAdjointObjIsDefined
5050

51-
@[deprecated (since := "2025-03-06")]
52-
alias PullbackObjIsDefined := pullbackObjIsDefined
53-
5451
end
5552

5653
section

0 commit comments

Comments
 (0)