feat(RingTheory/NonUnitalSubsemiring): point-free statement of centra…

…lity (#9053)

Also adds `isMulCentral_iff` using `mk_iff`.

Mathlib/Algebra/Group/Hom/Instances.lean

@@ -331,6 +331,14 @@ theorem AddMonoidHom.map_mul_iff (f : R →+ S) :
   Iff.symm AddMonoidHom.ext_iff₂
 #align add_monoid_hom.map_mul_iff AddMonoidHom.map_mul_iff
 
+lemma AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute {a : R} :
+    mulLeft a = mulRight a ↔ ∀ b, Commute a b :=
+  FunLike.ext_iff
+
+lemma AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute {b : R} :
+    mulRight b = mulLeft b ↔ ∀ a, Commute a b :=
+  FunLike.ext_iff
+
 /-- The left multiplication map: `(a, b) ↦ a * b`. See also `AddMonoidHom.mulLeft`. -/
 @[simps!]
 def AddMonoid.End.mulLeft : R →+ AddMonoid.End R :=
@@ -345,10 +353,6 @@ def AddMonoid.End.mulRight : R →+ AddMonoid.End R :=
 #align add_monoid.End.mul_right AddMonoid.End.mulRight
 #align add_monoid.End.mul_right_apply_apply AddMonoid.End.mulRight_apply_apply
 
-lemma AddMonoid.End.mulRight_eq_mulLeft_of_commute (a : R) (h : ∀ (b : R), Commute a b) :
-    mulRight a = mulLeft a :=
-  AddMonoidHom.ext fun _ ↦ (h _).eq.symm
-
 end Semiring
 
 section CommSemiring
@@ -357,9 +361,9 @@ variable {R S : Type*} [NonUnitalNonAssocCommSemiring R]
 
 namespace AddMonoid.End
 
-lemma comm_mulRight_eq_mulLeft : mulRight = (mulLeft : R →+ AddMonoid.End R) := by
-  ext a
-  exact mulRight_eq_mulLeft_of_commute _ (Commute.all _)
+lemma mulRight_eq_mulLeft : mulRight = (mulLeft : R →+ AddMonoid.End R) :=
+  AddMonoidHom.ext fun _ =>
+    Eq.symm <| AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute.2 (.all _)
 
 end AddMonoid.End
 

Mathlib/GroupTheory/Subsemigroup/Center.lean

@@ -56,6 +56,11 @@ structure IsMulCentral [Mul M] (z : M) : Prop where
   /-- associative property for right multiplication -/
   right_assoc (a b : M) : (a * b) * z = a * (b * z)
 
+-- TODO: these should have explicit arguments (mathlib4#9129)
+attribute [mk_iff isMulCentral_iff] IsMulCentral
+attribute [mk_iff isAddCentral_iff] IsAddCentral
+attribute [to_additive existing] isMulCentral_iff
+
 namespace IsMulCentral
 
 variable {a b c : M} [Mul M]

Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

@@ -494,6 +494,19 @@ instance center.instNonUnitalCommSemiring : NonUnitalCommSemiring (center R) :=
   { Subsemigroup.center.commSemigroup,
     NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring (center R) with }
 
+/-- A point-free means of proving membership in the center, for a non-associative ring.
+
+This can be helpful when working with types that have ext lemmas for `R →+ R`. -/
+lemma _root_.Set.mem_center_iff_addMonoidHom (a : R) :
+    a ∈ Set.center R ↔
+      AddMonoidHom.mulLeft a = .mulRight a ∧
+      AddMonoidHom.compr₂ .mul (.mulLeft a) = .comp .mul (.mulLeft a) ∧
+      AddMonoidHom.comp .mul (.mulRight a) = .compl₂ .mul (.mulLeft a) ∧
+      AddMonoidHom.compr₂ .mul (.mulRight a) = .compl₂ .mul (.mulRight a) := by
+  rw [Set.mem_center_iff, isMulCentral_iff]
+  simp_rw [FunLike.ext_iff]
+  rfl
+
 end NonUnitalNonAssocSemiring
 
 section NonUnitalSemiring