ι : Type u'
ι' : Type ?u.1242248
R : Type ?u.1242251
K : Type u_1
M : Type ?u.1242257
M' : Type ?u.1242260
M'' : Type ?u.1242263
V : Type u
V' : Type ?u.1242268
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.cons x v ∘ ↑(finSuccEquiv n).symm) ∘ some) ∧
      ¬(Fin.cons x v ∘ ↑(finSuccEquiv n).symm) none ∈ span K (range ((Fin.cons x v ∘ ↑(finSuccEquiv n).symm) ∘ some)) ↔
    LinearIndependent K v ∧ ¬x ∈ span K (range v)
ι : Type u'
ι' : Type ?u.1242248
R : Type ?u.1242251
K : Type u_1
M : Type ?u.1242257
M' : Type ?u.1242260
M'' : Type ?u.1242263
V : Type u
V' : Type ?u.1242268
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.cons x v) ↔ LinearIndependent K v ∧ ¬x ∈ span K (range v)
rw [← linearIndependent_equiv (finSuccEquiv n).symm, linearIndependent_option]
no goals
ι : Type u'
ι' : Type ?u.1242248
R : Type ?u.1242251
K : Type u_1
M : Type ?u.1242257
M' : Type ?u.1242260
M'' : Type ?u.1242263
V : Type u
V' : Type ?u.1242268
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.cons x v ∘ ↑(finSuccEquiv n).symm) ∘ some) ∧
      ¬(Fin.cons x v ∘ ↑(finSuccEquiv n).symm) none ∈ span K (range ((Fin.cons x v ∘ ↑(finSuccEquiv n).symm) ∘ some)) ↔
    LinearIndependent K v ∧ ¬x ∈ span K (range v)
exact Iff.rfl