Theorems · Theorem · ring theory

Finsupp.liftAddHom_apply_single

∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : α → M →+ N)
  (a : α) (b : M), ((Finsupp.liftAddHom f) fun₀ | a => b) = (f a) b

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddZeroClassAddCommMonoid