Theorems · Theorem · group theory

DirectSum.of_apply

∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {i : ι} (j : ι)
  (x : β i), ((DirectSum.of β i) x) j = if h : i = j then Eq.recOn h x else 0

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidableEq