ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
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
hs : LinearIndependent K fun b => ↑b
hx : ¬x ∈ span K s
⊢ LinearIndependent K fun b => ↑b
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
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
hs : LinearIndependent K fun b => ↑b
hx : ¬x ∈ span K s
⊢ LinearIndependent K fun b => ↑b
rw [← union_singleton]
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
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
hs : LinearIndependent K fun b => ↑b
hx : ¬x ∈ span K s
x0 : x ≠ 0
⊢ LinearIndependent K fun b => ↑b
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
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
hs : LinearIndependent K fun b => ↑b
hx : ¬x ∈ span K s
⊢ LinearIndependent K fun b => ↑b
have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem (span K s)) hx
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
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
hs : LinearIndependent K fun b => ↑b
hx : ¬x ∈ span K s
x0 : x ≠ 0
⊢ Disjoint (span K s) (span K {x})
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
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
hs : LinearIndependent K fun b => ↑b
hx : ¬x ∈ span K s
x0 : x ≠ 0
⊢ LinearIndependent K fun b => ↑b
apply hs.union (linearIndependent_singleton x0)
no goals
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
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
hs : LinearIndependent K fun b => ↑b
hx : ¬x ∈ span K s
x0 : x ≠ 0
⊢ Disjoint (span K s) (span K {x})
rwa [disjoint_span_singleton' x0]
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z : V
hs : LinearIndependent K fun b => ↑b
hx : ¬0 ∈ span K s
⊢ 0 ∈ span K s
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
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
hs : LinearIndependent K fun b => ↑b
hx : ¬x ∈ span K s
⊢ x = 0 → x ∈ span K s
rintro rfl
no goals
ι : Type u'
ι' : Type ?u.1209871
R : Type ?u.1209874
K : Type u_1
M : Type ?u.1209880
M' : Type ?u.1209883
M'' : Type ?u.1209886
V : Type u
V' : Type ?u.1209891
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z : V
hs : LinearIndependent K fun b => ↑b
hx : ¬0 ∈ span K s
⊢ 0 ∈ span K s
apply zero_mem (span K s)