isCancelMulZero_iff_forall_isRegular

English

In a semigroup with zero, the no-zero-divisors condition is equivalent to every nonzero element being regular.

Русский

В полугруппе с нулём условие отсутствия нулевых делителей эквивалентно тому, что каждый ненулевой элемент является регулярным.

LaTeX

$$$\operatorname{IsCancelMulZero}(M_0) \iff \forall a \in M_0,\ a \neq 0 \Rightarrow \operatorname{IsRegular}(a)$$$

Lean4

theorem isCancelMulZero_iff_forall_isRegular {M₀} [Mul M₀] [Zero M₀] :
    IsCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a :=
  by
  simp only [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff, ← forall_and]
  exact forall₂_congr fun _ _ ↦ isRegular_iff.symm

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