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