Theorems · Theorem · geometry

Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one

∀ {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} (s : Finset ι) (w : ι → k) (p : ι → P),
  ∑ i ∈ s, w i = 1 → ∀ (b : P), (Finset.affineCombination k s p) w = (s.weightedVSubOfPoint p b) w +ᵥ b

affineCombination gives the sum with any base point, when the sum of the weights is 1.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Combination

Cited by

12 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsor