liftAddHom_comp_single — Mathlib

English

Composition with a singleton adds up: (liftAddHom f) ∘ (singleAddHom a) equals f a.

Русский

Композицией с единичным отображением: (liftAddHom f) ∘ (singleAddHom a) = f(a).

LaTeX

$$$$ (\mathrm{liftAddHom} \ f).comp (\mathrm{singleAddHom} \ a) = f(a). $$$$

Lean4

@[simp]
theorem liftAddHom_comp_single [AddZeroClass M] [AddCommMonoid N] (f : α → M →+ N) (a : α) :
    ((liftAddHom (α := α) (M := M) (N := N)) f).comp (singleAddHom a) = f a :=
  AddMonoidHom.ext fun b => liftAddHom_apply_single f a b

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