comp_liftAddHom — Mathlib

English

g ∘ liftAddHom f equals liftAddHom (a ↦ g ∘ f a).

Русский

Сложение через liftAddHom совместимо: композиция с g эквивалентна liftAddHom от композиции g∘f.

LaTeX

$$$ g \\circ \\operatorname{liftAddHom} f = \\operatorname{liftAddHom} (\\lambda a. g \\circ f a). $$$

Lean4

/-- The `DFinsupp` version of `Finsupp.comp_liftAddHom` -/
theorem comp_liftAddHom {δ : Type*} [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ] (g : γ →+ δ)
    (f : ∀ i, β i →+ γ) : g.comp (liftAddHom f) = liftAddHom fun a => g.comp (f a) :=
  liftAddHom.symm_apply_eq.1 <|
    funext fun a => by rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

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