not_zero_iff — Mathlib

English

If M is nontrivial, then 0 is not M-regular.

Русский

Если модуль M не тривиален, то 0 не является M-регулярным.

LaTeX

$$$\neg IsSMulRegular M (0 : R) \Rightarrow Nontrivial M$$$

Lean4

/-- The `0` element is not `M`-regular, on a non-trivial module. -/
theorem not_zero_iff : ¬IsSMulRegular M (0 : R) ↔ Nontrivial M :=
  by
  rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]
  push_neg
  exact Iff.rfl

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