liftAddHom_comp_single — Mathlib

English

The composition of liftAddHom with singleAddHom β i equals the i-th component map f_i.

Русский

Композиция liftAddHom и singleAddHom β i даёт i-й компонентный отображение.

LaTeX

$$$ (liftAddHom f).\\mathrm{comp} (\\mathrm{singleAddHom } β i) = f_i. $$$

Lean4

/-- The `DFinsupp` version of `Finsupp.liftAddHom_comp_single` -/
theorem liftAddHom_comp_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ) (i : ι) :
    (liftAddHom f).comp (singleAddHom β i) = f i := by simp

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