Theorems · Definition · geometry

Finset.centroid

(k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : DivisionRing k] →
        [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → {ι : Type u_4} → Finset ι → (ι → P) → P

The centroid of some points. Although defined for any s, this is intended to be used in the case where the number of points, converted to k, is not zero.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Centroid

Cited by

45 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModuleAddTorsor