Theorems · Theorem · linear algebra

Finsupp.lmapDomain_comp

∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_9} {α'' : Type u_10} (f : α → α') (g : α' → α''),
  Finsupp.lmapDomain M R (g ∘ f) = Finsupp.lmapDomain M R g ∘ₗ Finsupp.lmapDomain M R f

Defined in

Mathlib.LinearAlgebra.Finsupp.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule