Theorems · Theorem · group theory

DirectSum.coe_of_apply

∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike S M]
  [inst_3 : AddSubmonoidClass S M] {A : ι → S} (i j : ι) (x : ↥(A i)),
  ↑(((DirectSum.of (fun i => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidSetLikeAddSubmonoidClass