English
If R is a domain, there exists a subset s of M such that #s = rank_R M and s is linearly independent (LinearIndepOn R id s).
Русский
Пусть R — область; существует подмножество s ⊆ M такое, что #s = rank_R M и s линейно независимо (LinearIndepOn R id s).
LaTeX
$$$\exists s \subseteq M\,\,\#s = \operatorname{Module.rank} R M \land \operatorname{LinearIndepOn} R \mathrm{id} s$$$
Lean4
theorem exists_set_linearIndependent_of_isDomain [IsDomain R] :
∃ s : Set M, #s = Module.rank R M ∧ LinearIndepOn R id s :=
by
obtain ⟨w, hw⟩ :=
IsLocalizedModule.linearIndependent_lift R⁰ (LocalizedModule.mkLinearMap R⁰ M) <|
Module.Free.chooseBasis (FractionRing R) (LocalizedModule R⁰ M) |>.linearIndependent.restrict_scalars' _
refine ⟨Set.range w, ?_, (linearIndepOn_id_range_iff hw.injective).mpr hw⟩
apply Cardinal.lift_injective.{max uR uM}
rw [Cardinal.mk_range_eq_of_injective hw.injective, ← Module.Free.rank_eq_card_chooseBasisIndex,
IsLocalization.rank_eq (FractionRing R) R⁰ le_rfl,
IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl]
