Theorems · Theorem · general algebraic systems

Finsupp.mapDomain_smul

∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_6} [inst : AddCommMonoid M] [inst_1 : DistribSMul R M]
  {f : α → β} (b : R) (v : α →₀ M), Finsupp.mapDomain f (b • v) = b • Finsupp.mapDomain f v

Defined in

Mathlib.Data.Finsupp.SMul

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDistribSMul