Theorems · Theorem · linear algebra

LinearMap.lsum_single

∀ (R : Type u) {ι : 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 : Fintype ι] [inst_5 : Semiring S]
  [inst_6 : (i : ι) → Module S (φ i)] [inst_7 : ∀ (i : ι), SMulCommClass R S (φ i)],
  (LinearMap.lsum R φ S) (LinearMap.single R φ) = LinearMap.id

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEqFintypeSemiringModuleSMulCommClass