all — Mathlib

English

If all multiplications cancel then every element is regular (both left and right).

Русский

Если все умножения отменяются, то каждый элемент регулярен (слева и справа).

LaTeX

$$$\text{IsRegular}(g)$ holds for all g whenever $\text{IsCancelMul}$ holds.$$

Lean4

/-- If all multiplications cancel then every element is regular. -/
@[to_additive /-- If all additions cancel then every element is add-regular. -/
    ]
theorem all [Mul R] [IsCancelMul R] (g : R) : IsRegular g :=
  ⟨.all g, .all g⟩

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