English
If b is a linearly independent family, finrank of span equals the index cardinal.
Русский
Если семейство несовпадений линейно независимо, finrank span равен мощности индекса.
LaTeX
$$$ [Nontrivial R] {\\iota : Type^*} [Fintype \\iota] {b : \\iota \\to M} (hb : LinearIndependent R b) : \\\\n \\text{finrank } R (\\operatorname{span}_R (\\operatorname{Set.range} b)) = Fintype.card \\iota. $$$
Lean4
theorem finrank_span_eq_card [Nontrivial R] {ι : Type*} [Fintype ι] {b : ι → M} (hb : LinearIndependent R b) :
finrank R (span R (Set.range b)) = Fintype.card ι :=
finrank_eq_of_rank_eq
(by
have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb
rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
lift_eq_nat_iff] at this)
