k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.492907
s : Finset ι
ι₂ : Type ?u.492913
s₂ : Finset ι₂
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.492907
s : Finset ι
ι₂ : Type ?u.492913
s₂ : Finset ι₂
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
rw [univ_fin2]
no goals
k : Type u_1
V : Type u_3
P : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type ?u.492907
s : Finset ι
ι₂ : Type ?u.492913
s₂ : Finset ι₂
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
convert centroid_pair k p 0 1