Theorems · Theorem · linear algebra

DFinsupp.coprodMap_apply

∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] [inst_6 : (x : N) → Decidable (x ≠ 0)] (f : (i : ι) → M i →ₗ[R] N)
  (x : Π₀ (i : ι), M i), (DFinsupp.coprodMap f) x = (DFinsupp.mapRange (fun i => ⇑(f i)) ⋯ x).sum fun x => id

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModuleDecidableEqDecidable