Commit 2023-12-18 04:53 4abd905e

View on Github →

feat(RingTheory/NonUnitalSubsemiring): point-free statement of centrality (#9053) Also adds isMulCentral_iff using mk_iff.

Estimated changes

Modified Mathlib/Algebra/Group/Hom/Instances.lean

deleted theorem AddMonoid.End.comm_mulRight_eq_mulLeft

added theorem AddMonoid.End.mulRight_eq_mulLeft

deleted theorem AddMonoid.End.mulRight_eq_mulLeft_of_commute

added theorem AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute

added theorem AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute

Modified Mathlib/GroupTheory/Subsemigroup/Center.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

added theorem Set.mem_center_iff_addMonoidHom