Theorems · Theorem · linear algebra

Module.piEquiv_apply_apply

∀ (ι : Type u_5) (R : Type u_6) (M : Type u_7) [inst : Fintype ι] [inst_1 : CommSemiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : ι → M) (w : ι → R), ((Module.piEquiv ι R M) v) w = ∑ i, w i • v i

Defined in

Mathlib.LinearAlgebra.StdBasis

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeCommSemiringAddCommMonoidModule