English
Two elements a and b are regular if and only if both products a*b and b*a are regular.
Русский
Два элемента a и b регуляренны тогда и только тогда, когда регуляренны и произведение a*b, и произведение b*a.
LaTeX
$$$ IsRegular (a * b) \land IsRegular (b * a) \leftrightarrow IsRegular a \land IsRegular b $$$
Lean4
/-- Two elements `a` and `b` are regular if and only if both products `a * b` and `b * a`
are regular. -/
@[to_additive /-- Two elements `a` and `b` are add-regular if and only if both sums `a + b` and
`b + a` are add-regular. -/
]
theorem isRegular_mul_and_mul_iff : IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b :=
by
refine ⟨?_, ?_⟩
· rintro ⟨ab, ba⟩
exact
⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩
· rintro ⟨ha, hb⟩
exact ⟨ha.mul hb, hb.mul ha⟩
