sum_circumcenterWeightsWithCircumcenter

English

The sum of circumcenterWeightsWithCircumcenter over all indices equals 1.

Русский

Сумма circumcenterWeightsWithCircumcenter по всем индексам равна 1.

LaTeX

$$$\sum_i circumcenterWeightsWithCircumcenter\; i = 1$$$

Lean4

/-- `circumcenterWeightsWithCircumcenter` sums to 1. -/
@[simp]
theorem sum_circumcenterWeightsWithCircumcenter (n : ℕ) : ∑ i, circumcenterWeightsWithCircumcenter n i = 1 := by
  classical
  convert sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [circumcenterWeightsWithCircumcenter]
  · simp

Похожие утверждения