rank_pos_of_free — Mathlib

English

If M is a nontrivial free module, then its rank is positive: 0 < rank_R M.

Русский

Если M — ненулевая свободная модуля, то её ранг положителен: 0 < rank_R M.

LaTeX

$$$[\text{Module.Free } R M] \land [\text{Nontrivial } M] \Rightarrow 0 < \operatorname{rank}_R M.$$$

Lean4

theorem rank_pos_of_free [Module.Free R M] [Nontrivial M] : 0 < Module.rank R M :=
  have := Module.nontrivial R M
  (pos_of_ne_zero <| Cardinal.mk_ne_zero _).trans_le (Free.chooseBasis R M).linearIndependent.cardinal_le_rank

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