no goals
ι : Type u'
ι' : Type ?u.1244590
R : Type ?u.1244593
K : Type u_1
M : Type ?u.1244599
M' : Type ?u.1244602
M'' : Type ?u.1244605
V : Type u
V' : Type ?u.1244610
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.snoc v x) ↔ LinearIndependent K v ∧ ¬x ∈ span K (range v)
erw [Fin.snoc_eq_cons_rotate, linearIndependent_equiv, linearIndependent_fin_cons]