nontrivial_of_finrank_eq_succ — Mathlib

English

A finite-dimensional space that is a subsingleton has finrank zero.

Русский

Конечномерное пространство, являющееся подмножеством-одиночкой, имеет finrank = 0.

LaTeX

$$$[\text{Subsingleton } M] \Rightarrow \operatorname{finrank} R M = 0$$$

Lean4

/-- A finite-dimensional space is nontrivial if it has `finrank` equal to the successor of a
natural number. -/
theorem nontrivial_of_finrank_eq_succ {n : ℕ} (hn : finrank R M = n.succ) : Nontrivial M :=
  nontrivial_of_finrank_pos (R := R) (by rw [hn]; exact n.succ_pos)

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