not_isLeftRegular_zero — Mathlib

English

In a nontrivial ring, 0 is not left-regular (with typeclass assumptions).

Русский

В несжатом кольце ноль не является левым регулярным (с учетом типовых предположений).

LaTeX

$$$\lnot IsLeftRegular(0) \,$$$

Lean4

/-- In a non-trivial ring, the element `0` is not left-regular -- with typeclasses. -/
theorem not_isLeftRegular_zero [nR : Nontrivial R] : ¬IsLeftRegular (0 : R) :=
  not_isLeftRegular_zero_iff.mpr nR

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