sum_centroidWeights_eq_one_of_nonempty

English

In characteristic zero, if s is nonempty, the centroid weights sum to 1: ∑_{i∈s} s.centroidWeights(k,i) = 1.

Русский

В характеристике ноль, если s не пусто, сумма весов центроида равна 1: ∑_{i∈s} s.centroidWeights(k,i) = 1.

LaTeX

$$$[CharZero\\ k] \\;\\Rightarrow\\; s.Nonempty \\Rightarrow \\sum_{i\\in s} s.centroidWeights(k,i) = 1$$$

Lean4

/-- In the characteristic zero case, the weights in the centroid sum
to 1 if the set is nonempty. -/
theorem sum_centroidWeights_eq_one_of_nonempty [CharZero k] (h : s.Nonempty) : ∑ i ∈ s, s.centroidWeights k i = 1 :=
  s.sum_centroidWeights_eq_one_of_card_ne_zero k (ne_of_gt (card_pos.2 h))

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