finrank_eq_zero_iff_isTorsion — Mathlib

English

For a finite R-module M, finrank R M = 0 iff M is a torsion R-module.

Русский

Для конечномерного R-модуля M верно: finrank R M = 0 тогда и только тогда, когда M — torsion-модуль над R.

LaTeX

$$$\\operatorname{finrank} R M = 0 \\;\\Leftrightarrow\\; \\text{Module.IsTorsion } R M$$$

Lean4

/-- The `StrongRankCondition` is automatic. See `commRing_strongRankCondition`. -/
theorem finrank_eq_zero_iff_isTorsion [StrongRankCondition R] [Module.Finite R M] :
    finrank R M = 0 ↔ Module.IsTorsion R M :=
  by
  rw [← rank_eq_zero_iff_isTorsion (R := R), ← finrank_eq_rank]
  norm_cast

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