isRegular_mul_iff — Mathlib

English

In a commutative semigroup, a*b is regular if and only if a and b are regular.

Русский

В коммутативной полугруппе произведение a*b регулярен тогда и только тогда, когда a и b регуляренны.

LaTeX

$$$ IsRegular (a * b) \leftrightarrow IsRegular a \land IsRegular b $$$

Lean4

/-- A product is regular if and only if the factors are. -/
@[to_additive /-- A sum is add-regular if and only if the summands are. -/
    ]
theorem isRegular_mul_iff : IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b :=
  by
  refine Iff.trans ?_ isRegular_mul_and_mul_iff
  exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩

Похожие утверждения