English
The same relation as finrank_eq_card_chooseBasisIndex, with root qualification.
Русский
Та же зависимость, что и выше, с префиксом корня.
LaTeX
$$$\\operatorname{finrank}_R M = \\mathrm{Fintype.card}(\\mathrm{ChooseBasisIndex}\\, R\, M)$$$
Lean4
/-- The rank of a free module `M` over an infinite scalar ring `R` is the cardinality of `M`
whenever `#R < #M`. -/
theorem rank_eq_mk_of_infinite_lt [Infinite R] (h_lt : lift.{v} #R < lift.{u} #M) : Module.rank R M = #M :=
by
have : Infinite M := infinite_iff.mpr <| lift_le.mp <| le_trans (by simp) h_lt.le
have h : lift #M = lift #(ChooseBasisIndex R M →₀ R) := lift_mk_eq'.mpr ⟨(chooseBasis R M).repr⟩
simp only [mk_finsupp_lift_of_infinite', ← rank_eq_card_chooseBasisIndex, lift_max, lift_lift] at h
refine lift_inj.mp ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ ?_).left
exact (lift_umax.{v, u}.symm ▸ h_lt).ne
