liftAddHom_singleAddHom — Mathlib

English

The lift of singletonAddHom across coordinates is the identity map on the DFinsupp space.

Русский

Обобщение через liftAddHom над единичным дополнением даёт тождественный отображение на DFinsupp.

LaTeX

$$$ \\operatorname{liftAddHom} (\\text{singleAddHom } β) = \\operatorname{id}_{\\Pi_{0 i} β_i}. $$$

Lean4

/-- The `DFinsupp` version of `Finsupp.liftAddHom_singleAddHom` -/
theorem liftAddHom_singleAddHom [∀ i, AddCommMonoid (β i)] :
    liftAddHom (singleAddHom β) = AddMonoidHom.id (Π₀ i, β i) :=
  liftAddHom.toEquiv.apply_eq_iff_eq_symm_apply.2 rfl

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