mk_eq_rank'' — Mathlib

English

For any basis v: ι → M, the cardinality of ι equals the rank of M, i.e., |ι| = rank_R(M).

Русский

Для любого базиса v: ι → M кардинальность множества индексов ι равна рангу модуля M: |ι| = rank_R(M).

LaTeX

$$$|\\iota| = \\operatorname{rank}_R(M)$$$

Lean4

theorem mk_eq_rank'' {ι : Type v} (v : Basis ι R M) : #ι = Module.rank R M :=
  by
  haveI := nontrivial_of_invariantBasisNumber R
  rw [Module.rank_def]
  apply le_antisymm
  · trans
    swap
    · apply le_ciSup (Cardinal.bddAbove_range _)
      exact
        ⟨Set.range v, by
          rw [LinearIndepOn]
          convert v.reindexRange.linearIndependent
          simp⟩
    · exact (Cardinal.mk_range_eq v v.injective).ge
  · apply ciSup_le'
    rintro ⟨s, li⟩
    apply linearIndependent_le_basis v _ li

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