Theorems · Theorem · geometry

Finset.affineCombination_eq_linear_combination

∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  (s : Finset ι) (p : ι → V) (w : ι → k), ∑ i ∈ s, w i = 1 → (Finset.affineCombination k s p) w = ∑ i ∈ s, w i • p i

Viewing a module as an affine space modelled on itself, affine combinations are just linear combinations.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Combination

Cited by

8 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule