Theorems · Theorem · commutative algebra

finsuppLEquivDirectSum_symm_lof

∀ (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 ι).symm ((DirectSum.lof R ι (fun x => M) i) m) = fun₀ | 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