finrank_pos_iff_exists_ne_zero — Mathlib

English

A finite-dimensional module has 0 < finrank iff it is nontrivial.

Русский

Конечномерный модуль имеет 0 < finrank тогда и только тогда, когда он ненулевой.

LaTeX

$$$0 < \operatorname{finrank} R M \;\iff\; \text{Nontrivial } M$$$

Lean4

/-- A finite rank torsion-free module has positive `finrank` iff it has a nonzero element. -/
theorem finrank_pos_iff_exists_ne_zero [NoZeroSMulDivisors R M] : 0 < finrank R M ↔ ∃ x : M, x ≠ 0 :=
  by
  rw [← @rank_pos_iff_exists_ne_zero R M, ← finrank_eq_rank]
  norm_cast

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