Theorems · Theorem · geometry

Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero

∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] [inst_2 : Fintype ι],
  s.card ≠ 0 → ∑ i, Finset.centroidWeightsIndicator k s i = 1

In the characteristic zero case, the weights in the centroid indexed by a Fintype sum to 1 if the number of points is not zero.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Centroid

Cited by

0 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingCharZeroFintype