Theorems · Theorem · commutative algebra

lmap_finsuppLEquivDirectSum_eq

∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι : Type u_1)
  [inst_3 : DecidableEq ι] {N : Type u_2} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] (ε : M →ₗ[R] N) (m : ι →₀ M),
  (DirectSum.lmap fun x => ε) ((finsuppLEquivDirectSum R M ι) m) =
    (finsuppLEquivDirectSum R N ι) (Finsupp.mapRange ⇑ε ⋯ m)

Defined in

Mathlib.Algebra.DirectSum.Finsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEqAddCommMonoidModule