liftAddHom_apply_single — Mathlib

English

Lifting a pointwise additive homomorphism to finsupps sends a single to the evaluation value.

Русский

Поднятие аддитивного гомоморфизма к финспп отправляет единичный элемент в значение на этом индексе.

LaTeX

$$$$ (\mathrm{liftAddHom} \ (\alpha := \alpha) (M := M) (N := N)) \\ f (\mathrm{single} \ a \ b) = f(a,b). $$$$

Lean4

theorem liftAddHom_apply_single [AddZeroClass M] [AddCommMonoid N] (f : α → M →+ N) (a : α) (b : M) :
    (liftAddHom (α := α) (M := M) (N := N)) f (single a b) = f a b :=
  sum_single_index (f a).map_zero

Похожие утверждения