Theorems · Theorem · commutative algebra

finsuppLEquivDirectSum_single

∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι : Type u_1)
  [inst_3 : DecidableEq ι] (i : ι) (m : M),
  ((finsuppLEquivDirectSum R M ι) fun₀ | i => m) = (DirectSum.lof R ι (fun i => M) i) m

Defined in

Mathlib.Algebra.DirectSum.Finsupp

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEq