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.373329
R✝ : Type u
inst✝⁵ : Ring R✝
inst✝⁴ : StrongRankCondition R✝
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_1
inst✝¹ : Ring R
inst✝ : StrongRankCondition R
n m : ℕ
v : Fin m → Fin n → R
h : LinearIndependent R v
⊢ m ≤ n
simpa using linearIndependent_le_basis (Pi.basisFun R (Fin n)) v h