K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
b : Finset V
h : LinearIndependent K fun x => ↑x
⊢ Fintype.card { x // x ∈ b } ≤ finrank K V
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
b : Finset V
h : LinearIndependent K fun x => ↑x
⊢ Finset.card b ≤ finrank K V
rw [← Fintype.card_coe]
no goals
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
b : Finset V
h : LinearIndependent K fun x => ↑x
⊢ Fintype.card { x // x ∈ b } ≤ finrank K V
exact fintype_card_le_finrank_of_linearIndependent h