Theorems · Theorem · linear algebra

LinearMap.lsum_piSingle

∀ (R : Type u) {M : Type v} {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (S : Type u_1) [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Fintype ι] [inst_7 : Semiring S] [inst_8 : Module S M] [inst_9 : SMulCommClass R S M]
  (f : (i : ι) → φ i →ₗ[R] M) (i : ι) (x : φ i), ((LinearMap.lsum R φ S) f) (Pi.single i x) = (f i) x

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEqAddCommMonoidModuleFintypeSemiringModuleSMulCommClass