nontrivial_of_finrank_pos — Mathlib

English

Bound for iSupIndep auxiliary: lift of cardinality of nonzero submodules ≤ finrank.

Русский

Граница для iSupIndep: кардинал ненулевых подпредметов не больше finrank.

LaTeX

$$$\forall p : ι \to \text{Submodule}_R M,\; \text{hp} : \text{iSupIndep } p\Rightarrow \operatorname{Cardinal}.lift(\#\{ i : ι // p(i) \neq \bot \}) \le (\operatorname{finrank} R M).cast$$$

Lean4

/-- A finite-dimensional space is nontrivial if it has positive `finrank`. -/
theorem nontrivial_of_finrank_pos (h : 0 < finrank R M) : Nontrivial M :=
  rank_pos_iff_nontrivial.mp (lt_rank_of_lt_finrank h)

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