Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-09 14:51
d662e6c3
View on Github →
chore(*): drop some long-deprecated theorems (
#13619
)
Estimated changes
Modified
Mathlib/Algebra/BigOperators/Finsupp.lean
Modified
Mathlib/Algebra/BigOperators/Group/List.lean
Modified
Mathlib/Algebra/Category/MonCat/Limits.lean
Modified
Mathlib/Algebra/Group/Equiv/Basic.lean
Modified
Mathlib/Algebra/Group/Hom/Defs.lean
deleted
theorem
MonoidHom.coe_inj
deleted
theorem
MonoidHom.congr_arg
deleted
theorem
MonoidHom.congr_fun
deleted
theorem
MonoidHom.ext_iff
deleted
theorem
MulHom.coe_inj
deleted
theorem
MulHom.congr_arg
deleted
theorem
MulHom.congr_fun
deleted
theorem
MulHom.ext_iff
deleted
theorem
OneHom.coe_inj
deleted
theorem
OneHom.congr_arg
deleted
theorem
OneHom.congr_fun
deleted
theorem
OneHom.ext_iff
Modified
Mathlib/Algebra/Group/Pi/Basic.lean
deleted
theorem
Pi.bit0_apply
deleted
theorem
Pi.bit1_apply
Modified
Mathlib/Algebra/GroupWithZero/Hom.lean
deleted
theorem
MonoidWithZeroHom.coe_inj
deleted
theorem
MonoidWithZeroHom.congr_arg
deleted
theorem
MonoidWithZeroHom.congr_fun
deleted
theorem
MonoidWithZeroHom.ext_iff
Modified
Mathlib/Algebra/Ring/Hom/Defs.lean
modified
theorem
NonUnitalRingHom.coe_mulHom_injective
modified
theorem
RingHom.coe_monoidHom_injective
Modified
Mathlib/Data/DFinsupp/Basic.lean
deleted
theorem
DFinsupp.coeFn_injective
deleted
theorem
DFinsupp.ext_iff
Modified
Mathlib/Data/ENNReal/Basic.lean
deleted
theorem
ENNReal.exists_ne_top'
modified
theorem
ENNReal.exists_ne_top
Modified
Mathlib/Data/Finsupp/Defs.lean
deleted
theorem
Finsupp.coeFn_inj
deleted
theorem
Finsupp.coeFn_injective
deleted
theorem
Finsupp.congr_fun
deleted
theorem
Finsupp.ext_iff
Modified
Mathlib/Data/Int/Defs.lean
deleted
theorem
Int.natAbs_ne_zero_of_ne_zero
Modified
Mathlib/Data/Option/Basic.lean
added
theorem
Option.exists_ne_none
Modified
Mathlib/Data/Option/Defs.lean