finrank_pos_iff — Mathlib

English

For a finite module, finrank equals zero iff every vector is annihilated by some nonzero scalar.

Русский

Для конечномерного модуля finrank = 0 тогда и только тогда, когда каждый вектор уничтожается некоторым ненулевым скаляром.

LaTeX

$$$\operatorname{finrank} R M = 0 \iff \forall x \in M, \exists a \in R, a \neq 0 \land a \cdot x = 0$$$

Lean4

/-- An `R`-finite torsion-free module has positive `finrank` iff it is nontrivial. -/
theorem finrank_pos_iff [NoZeroSMulDivisors R M] : 0 < finrank R M ↔ Nontrivial M :=
  by
  rw [← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank]
  norm_cast

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