Commit 2024-11-12 05:36 bf637c80

View on Github →

chore: cleanup of simpNF (#18864) Lots more to go.

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

deleted theorem AlgHom.coe_to_nonUnitalAlgHom

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

Modified Mathlib/Algebra/Category/Grp/Biproducts.lean

Modified Mathlib/Algebra/Category/Grp/Limits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

Modified Mathlib/Algebra/Category/Ring/Adjunctions.lean

Modified Mathlib/Algebra/DirectSum/Internal.lean

modified theorem SetLike.GradeZero.coe_algebraMap

modified theorem SetLike.GradeZero.coe_natCast

modified theorem SetLike.GradeZero.coe_ofNat

Modified Mathlib/Algebra/Free.lean

Modified Mathlib/Algebra/GradedMonoid.lean

modified theorem SetLike.GradeZero.coe_mul

modified theorem SetLike.GradeZero.coe_one

modified theorem SetLike.GradeZero.coe_pow

Modified Mathlib/Algebra/GradedMulAction.lean

Modified Mathlib/Algebra/Group/Commute/Defs.lean

Modified Mathlib/Algebra/Group/Nat.lean

Modified Mathlib/Algebra/Group/Pi/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Defs.lean

Modified Mathlib/Algebra/Group/Units/Equiv.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean