Theorems · Theorem · geometry

AffineBasis.linear_combination_coord_eq_self

∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} [inst : AddCommGroup V] [inst_1 : Ring k] [inst_2 : Module k V]
  [inst_3 : Fintype ι] (b : AffineBasis ι k V) (v : V), ∑ i, (b.coord i) v • b i = v

A variant of AffineBasis.affineCombination_coord_eq_self for the special case when the affine space is a module so we can talk about linear combinations.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Basis

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupRingModuleFintype