English
If a simplex s is equilateral, then every angle at every triple of distinct vertices is exactly π/3.
Русский
Если тетраэдр/многоугольник s равносторонний, то каждый угол между любыми тремя различными вершинами равен π/3.
LaTeX
$$$\angle(s.points_{i_1}, s.points_{i_2}, s.points_{i_3}) = \frac{\pi}{3}$ for all distinct i1,i2,i3.$$
Lean4
theorem angle_eq_pi_div_three {s : Simplex ℝ P n} (he : s.Equilateral) {i₁ i₂ i₃ : Fin (n + 1)} (h₁₂ : i₁ ≠ i₂)
(h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : ∠ (s.points i₁) (s.points i₂) (s.points i₃) = π / 3 :=
by
rcases he with ⟨r, hr⟩
rw [angle, InnerProductGeometry.angle, real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two]
refine Real.arccos_eq_of_eq_cos (by linarith [Real.pi_nonneg]) (by linarith [Real.pi_nonneg]) ?_
simp only [vsub_sub_vsub_cancel_right, ← dist_eq_norm_vsub, hr _ _ h₁₂, hr _ _ h₁₃, hr _ _ h₂₃.symm,
Real.cos_pi_div_three]
have hr0 : r ≠ 0 := by
rintro rfl
replace hr := hr _ _ h₁₂
rw [dist_eq_zero] at hr
exact h₁₂ (s.independent.injective hr)
field_simp
ring
