Theorems · Theorem · general algebraic systems

Finsupp.smul_single

∀ {α : Type u_1} {M : Type u_5} {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M] (c : R) (a : α) (b : M),
  (c • fun₀ | a => b) = fun₀ | a => c • b

Defined in

Mathlib.Data.Finsupp.SMulWithZero

Cited by

48 results in Mathlib

Foundations

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

Assumes

ZeroSMulZeroClass