rank_eq_zero_iff_isTorsion — Mathlib

English

For a module M over a domain R, the rank is zero if and only if M is a torsion module.

Русский

Для модуля M над доменом R ранг равен нулю тогда и только тогда, когда M является torsion-модулем.

LaTeX

$$$\\operatorname{Module.rank} R M = 0 \\;\\Leftrightarrow\\; M \\text{ is torsion over } R$$$

Lean4

theorem rank_eq_zero_iff_isTorsion : Module.rank R M = 0 ↔ Module.IsTorsion R M :=
  by
  rw [Module.IsTorsion, rank_eq_zero_iff]
  simp [mem_nonZeroDivisors_iff_ne_zero]

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