ι : Type u'
ι' : Type ?u.26530
R : Type u_1
K : Type ?u.26536
M : Type u_2
M' : Type ?u.26542
M'' : Type ?u.26545
V : Type u
V' : Type ?u.26550
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
⊢ (¬∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0) ↔
    ∃ s g, ∑ i in s, g i • v i = 0 ∧ ∃ i, i ∈ s ∧ g i ≠ 0
ι : Type u'
ι' : Type ?u.26530
R : Type u_1
K : Type ?u.26536
M : Type u_2
M' : Type ?u.26542
M'' : Type ?u.26545
V : Type u
V' : Type ?u.26550
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
⊢ ¬LinearIndependent R v ↔ ∃ s g, ∑ i in s, g i • v i = 0 ∧ ∃ i, i ∈ s ∧ g i ≠ 0
rw [linearIndependent_iff']
no goals
ι : Type u'
ι' : Type ?u.26530
R : Type u_1
K : Type ?u.26536
M : Type u_2
M' : Type ?u.26542
M'' : Type ?u.26545
V : Type u
V' : Type ?u.26550
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
⊢ (¬∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0) ↔
    ∃ s g, ∑ i in s, g i • v i = 0 ∧ ∃ i, i ∈ s ∧ g i ≠ 0
simp only [exists_prop, not_forall]