K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hb : LinearIndependent K b
this : Module.rank K { x // x ∈ span K (Set.range b) } = (#↑(Set.range b))
⊢ Module.rank K { x // x ∈ span K (Set.range b) } = ↑(Fintype.card ι)
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hb : LinearIndependent K b
⊢ Module.rank K { x // x ∈ span K (Set.range b) } = ↑(Fintype.card ι)
have : Module.rank K (span K (Set.range b)) = (#Set.range b) := rank_span hb
no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hb : LinearIndependent K b
this : Module.rank K { x // x ∈ span K (Set.range b) } = (#↑(Set.range b))
⊢ Module.rank K { x // x ∈ span K (Set.range b) } = ↑(Fintype.card ι)
rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
  lift_eq_nat_iff] at this