ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ (fun r => r • 1) (g i) = (fun r => r • 1) 0
ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
⊢ LinearIndependent R v
refine' linearIndependent_iff'.mpr fun s g hg i hi => hinj _
ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i • 1 = 0 • 1
ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ (fun r => r • 1) (g i) = (fun r => r • 1) 0
dsimp only
ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i • 1 = 0
ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i • 1 = 0 • 1
rw [zero_smul]
ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ x in s, g x • v x = 0
ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ i in s, (fun x => g x • 1) i • v i = 0
simp_rw [smul_assoc, one_smul]
no goals
ι : Type u'
ι' : Type ?u.123510
R : Type u_2
K : Type u_1
M : Type u_3
M' : Type ?u.123522
M'' : Type ?u.123525
V : Type u
V' : Type ?u.123530
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✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ x in s, g x • v x = 0
exact hg