Theorems · Theorem · ring theory

DirectSum.component.of

∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i j : ι) (b : M j),
  (DirectSum.component R ι M i) ((DirectSum.lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0

Defined in

Mathlib.Algebra.DirectSum.Module

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEq