ι : Type u'
ι' : Type ?u.83214
R : Type u_1
K : Type ?u.83220
M : Type u_2
M' : Type ?u.83226
M'' : Type ?u.83229
V : Type u
V' : Type ?u.83234
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ ↑(Finsupp.single i 1) i = 0
ι : Type u'
ι' : Type ?u.83214
R : Type u_1
K : Type ?u.83220
M : Type u_2
M' : Type ?u.83226
M'' : Type ?u.83229
V : Type u
V' : Type ?u.83234
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ 1 = 0
suffices (Finsupp.single i 1 : ι →₀ R) i = 0 by simpa
ι : Type u'
ι' : Type ?u.83214
R : Type u_1
K : Type ?u.83220
M : Type u_2
M' : Type ?u.83226
M'' : Type ?u.83229
V : Type u
V' : Type ?u.83234
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ ↑0 i = 0

ι : Type u'
ι' : Type ?u.83214
R : Type u_1
K : Type ?u.83220
M : Type u_2
M' : Type ?u.83226
M'' : Type ?u.83229
V : Type u
V' : Type ?u.83234
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ ↑(Finsupp.total ι M R v) (Finsupp.single i 1) = 0
ι : Type u'
ι' : Type ?u.83214
R : Type u_1
K : Type ?u.83220
M : Type u_2
M' : Type ?u.83226
M'' : Type ?u.83229
V : Type u
V' : Type ?u.83234
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ ↑(Finsupp.single i 1) i = 0
rw [linearIndependent_iff.1 hv (Finsupp.single i 1)]
no goals
ι : Type u'
ι' : Type ?u.83214
R : Type u_1
K : Type ?u.83220
M : Type u_2
M' : Type ?u.83226
M'' : Type ?u.83229
V : Type u
V' : Type ?u.83234
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
this : ↑(Finsupp.single i 1) i = 0
⊢ 1 = 0
simpa
no goals
ι : Type u'
ι' : Type ?u.83214
R : Type u_1
K : Type ?u.83220
M : Type u_2
M' : Type ?u.83226
M'' : Type ?u.83229
V : Type u
V' : Type ?u.83234
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ ↑0 i = 0
simp
no goals
ι : Type u'
ι' : Type ?u.83214
R : Type u_1
K : Type ?u.83220
M : Type u_2
M' : Type ?u.83226
M'' : Type ?u.83229
V : Type u
V' : Type ?u.83234
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ ↑(Finsupp.total ι M R v) (Finsupp.single i 1) = 0
simp [h]