rank_pos_iff_nontrivial — Mathlib

English

The rank is positive exactly when the module is nontrivial (under suitable NoZeroSMulDivisors assumptions).

Русский

Ранг положителен тогда и только тогда, когда модуль не тривиален (при подходящих предпосылках NoZeroSMulDivisors).

LaTeX

$$$[\text{NoZeroSMulDivisors } R M] \Rightarrow (0 < \operatorname{rank}_R M \iff \text{Nontrivial } M).$$$

Lean4

theorem rank_pos_iff_nontrivial : 0 < Module.rank R M ↔ Nontrivial M :=
  rank_pos_iff_exists_ne_zero.trans (nontrivial_iff_exists_ne 0).symm

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