k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
j : ι
hp : LinearIndependent k fun i => p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i => ↑(AffineMap.lineMap (p j) (p ↑i)) ↑(w ↑i) -ᵥ ↑(AffineMap.lineMap (p j) (p j)) ↑(w j)
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
hp : AffineIndependent k p
j : ι
w : ι → kˣ
⊢ AffineIndependent k fun i => ↑(AffineMap.lineMap (p j) (p i)) ↑(w i)
rw [affineIndependent_iff_linearIndependent_vsub k _ j] at hp⊢
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
j : ι
hp : LinearIndependent k fun i => p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i => ↑(w ↑i) • (p ↑i -ᵥ p j)
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
j : ι
hp : LinearIndependent k fun i => p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i => ↑(AffineMap.lineMap (p j) (p ↑i)) ↑(w ↑i) -ᵥ ↑(AffineMap.lineMap (p j) (p j)) ↑(w j)
simp only [AffineMap.lineMap_vsub_left, AffineMap.coe_const, AffineMap.lineMap_same, const_apply]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
j : ι
hp : LinearIndependent k fun i => p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i => ↑(w ↑i) • (p ↑i -ᵥ p j)
exact hp.units_smul fun i => w i