ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
⊢ ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • (w • v) i = 0 → ∀ (i : ι), g i = 0
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : LinearIndependent R v
w : ι → Rˣ
⊢ LinearIndependent R (w • v)
rw [linearIndependent_iff''] at hv⊢
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ g i = 0
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
⊢ ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • (w • v) i = 0 → ∀ (i : ι), g i = 0
intro s g hgs hsum i
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ g i * ↑(w i) = 0
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ g i = 0
rw [← (w i).mul_left_eq_zero]
case refine'_1
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i✝ i : ι
hi : ¬i ∈ s
⊢ (fun i => g i • ↑(w i)) i = 0

case refine'_2
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ ∑ i in s, (fun i => g i • ↑(w i)) i • v i = 0
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ g i * ↑(w i) = 0
refine' hv s (fun i => g i • (w i : R)) (fun i hi => _) _ i
case refine'_1
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i✝ i : ι
hi : ¬i ∈ s
⊢ g i • ↑(w i) = 0
case refine'_1
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i✝ i : ι
hi : ¬i ∈ s
⊢ (fun i => g i • ↑(w i)) i = 0
dsimp only
no goals
case refine'_1
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i✝ i : ι
hi : ¬i ∈ s
⊢ g i • ↑(w i) = 0
exact (hgs i hi).symm ▸ zero_smul _ _
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ ∀ (x : ι), x ∈ s → (fun i => g i • ↑(w i)) x • v x = g x • (w • v) x
case refine'_2
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ ∑ i in s, (fun i => g i • ↑(w i)) i • v i = 0
rw [← hsum, Finset.sum_congr rfl _]
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i x✝ : ι
a✝ : x✝ ∈ s
⊢ (fun i => g i • ↑(w i)) x✝ • v x✝ = g x✝ • (w • v) x✝
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ ∀ (x : ι), x ∈ s → (fun i => g i • ↑(w i)) x • v x = g x • (w • v) x
intros
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i x✝ : ι
a✝ : x✝ ∈ s
⊢ g x✝ • ↑(w x✝) • v x✝ = g x✝ • w x✝ • v x✝
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i x✝ : ι
a✝ : x✝ ∈ s
⊢ (fun i => g i • ↑(w i)) x✝ • v x✝ = g x✝ • (w • v) x✝
erw [Pi.smul_apply, smul_assoc]
no goals
ι : Type u'
ι' : Type ?u.293271
R : Type u_1
K : Type ?u.293277
M : Type u_2
M' : Type ?u.293283
M'' : Type ?u.293286
V : Type u
V' : Type ?u.293291
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → Rˣ
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i x✝ : ι
a✝ : x✝ ∈ s
⊢ g x✝ • ↑(w x✝) • v x✝ = g x✝ • w x✝ • v x✝
rfl