finrank_pos — Mathlib

English

Same as above; finrank zero iff every vector has a nonzero scalar annihilator.

Русский

То же самое; finrank = 0 эквивалентно существованию ненулевого скаляра, который аннигилирует каждый вектор.

LaTeX

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

Lean4

/-- A nontrivial finite-dimensional space has positive `finrank`. -/
theorem finrank_pos [NoZeroSMulDivisors R M] [h : Nontrivial M] : 0 < finrank R M :=
  finrank_pos_iff.mpr h

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