Theorems · Definition · geometry

Finset.weightedVSubOfPoint

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

A weighted sum of the results of subtracting a base point from the given points, as a linear map on the weights. The main cases of interest are where the sum of the weights is 0, in which case the sum is independent of the choice of base point, and where the sum of the weights is 1, in which case the sum added to the base point is independent of the choice of base point.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Combination

Cited by

42 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsor