ι : Type u_1
ι' : Type ?u.122547
k : Type u_2
V : Type u_3
P : Type ?u.122556
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b✝ : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : (↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) v) = v
⊢ ∑ i : ι, ↑(coord b i) v • ↑b i = v
ι : Type u_1
ι' : Type ?u.122547
k : Type u_2
V : Type u_3
P : Type ?u.122556
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b✝ : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
⊢ ∑ i : ι, ↑(coord b i) v • ↑b i = v
have hb := b.affineCombination_coord_eq_self v
no goals
ι : Type u_1
ι' : Type ?u.122547
k : Type u_2
V : Type u_3
P : Type ?u.122556
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b✝ : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : (↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(coord b i) v) = v
⊢ ∑ i : ι, ↑(coord b i) v • ↑b i = v
rwa [Finset.univ.affineCombination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v)] at hb