no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.106262
R : Type u
inst✝⁷ : Ring R
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type v'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
M₁ : Type v
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
ι : Type v
v : ι → M
hv : LinearIndependent R v
⊢ (#ι) ≤ Module.rank R M
simpa using cardinal_lift_le_rank_of_linearIndependent hv