feat (Mathlib/Algebra/Regular/Basic.lean): Add lemmas on RightRegular (#9464)

XavierXarles · XavierXarles · commit 26ccd1e9cdd5 · 2024-01-05T18:57:29.000Z
A couple of lemmas on RightRegular that could be useful for future work on Localization
diff --git a/Mathlib/Algebra/Regular/Basic.lean b/Mathlib/Algebra/Regular/Basic.lean
@@ -88,6 +88,15 @@ theorem IsLeftRegular.right_of_commute {a : R}
   fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm
 #align is_left_regular.right_of_commute IsLeftRegular.right_of_commute
 
+theorem IsRightRegular.left_of_commute {a : R}
+    (ca : ∀ b, Commute a b) (h : IsRightRegular a) : IsLeftRegular a := by
+  simp_rw [@Commute.symm_iff R _ a] at ca
+  exact fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm
+
+theorem Commute.isRightRegular_iff {a : R} (ca : ∀ b, Commute a b) :
+    IsRightRegular a ↔ IsLeftRegular a :=
+  ⟨IsRightRegular.left_of_commute ca, IsLeftRegular.right_of_commute ca⟩
+
 theorem Commute.isRegular_iff {a : R} (ca : ∀ b, Commute a b) : IsRegular a ↔ IsLeftRegular a :=
   ⟨fun h => h.left, fun h => ⟨h, h.right_of_commute ca⟩⟩
 #align commute.is_regular_iff Commute.isRegular_iff
