not_isLeftRegular_zero_iff — Mathlib

English

In a nontrivial MulZeroClass, the element 0 is not left-regular.

Русский

В не тривиальном MulZeroClass ноль не является левым регулярным.

LaTeX

$$$\neg IsLeftRegular(0) \iff Nontrivial(R)$$$

Lean4

/-- In a non-trivial `MulZeroClass`, the `0` element is not left-regular. -/
theorem not_isLeftRegular_zero_iff : ¬IsLeftRegular (0 : R) ↔ Nontrivial R :=
  by
  rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]
  push_neg
  exact Iff.rfl

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