Theorems · Theorem · linear algebra

Module.Basis.equivFun_symm_apply

∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] (b : Module.Basis ι R M) (x : ι → R), b.equivFun.symm x = ∑ i, x i • b i

Given a basis v indexed by ι, the canonical linear equivalence between ι → R and M maps a function x : ι → R to the linear combination ∑_i x i • v i.

Defined in

Mathlib.LinearAlgebra.Basis.Defs

Cited by

22 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleFintype