toFinsupp_comp_toFreeAbelianGroup

English

A specific equality of the composite map on the canonical basis yields an equality with identity on FreeAbelianGroup X.

Русский

Конкретное равенство композиции отображений на базисе даёт равенство с тождественным на FreeAbelianGroup X.

LaTeX

$$toFreeAbelianGroup (toFinsupp) = AddMonoidHom.id (FreeAbelianGroup X)$$

Lean4

@[simp]
theorem toFinsupp_comp_toFreeAbelianGroup : toFinsupp.comp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ) :=
  by
  ext x y; simp only [AddMonoidHom.id_comp]
  rw [AddMonoidHom.comp_assoc, Finsupp.toFreeAbelianGroup_comp_singleAddHom]
  simp only [toFinsupp, AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply, one_smul, lift_apply_of,
    AddMonoidHom.flip_apply, smulAddHom_apply]

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