R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
refine' Iff.trans _ isRegular_mul_and_mul_iff
no goals
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)
refine' ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
no goals
R : Type u_1
inst✝ : CommSemigroup R
a b : R
ab : IsRegular (a * b)
⊢ IsRegular (b * a)
rwa [mul_comm]