rank_eq_ofNat_iff_finrank_eq_ofNat

English

For any M, rank_R M = 1 iff finrank_R M = 1 (alternative formulation).

Русский

Для любого M: ранг_R M = 1 эквивалентно finrank_R M = 1 (альтернативная формулировка).

LaTeX

$$$$\\operatorname{Module.rank}_R M = 1 \\\\iff \\\\operatorname{finrank}_R M = 1.$$$$

Lean4

/-- This is like `rank_eq_one_iff_finrank_eq_one` but works for `2`, `3`, `4`, ... -/
theorem rank_eq_ofNat_iff_finrank_eq_ofNat (n : ℕ) [Nat.AtLeastTwo n] :
    Module.rank R M = OfNat.ofNat n ↔ finrank R M = OfNat.ofNat n :=
  Cardinal.toNat_eq_ofNat.symm

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