toFreeAbelianGroup_comp_singleAddHom

English

The other direction also gives an identity: FreeAbelianGroup.toFinsupp ∘ FreeAbelianGroup.toFinsupp = id on FreeAbelianGroup X.

Русский

С другой стороны: FreeAbelianGroup.toFinsupp ∘ FreeAbelianGroup.toFinsupp = id на FreeAbelianGroup X.

LaTeX

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

Lean4

@[simp]
theorem toFreeAbelianGroup_comp_singleAddHom (x : X) :
    Finsupp.toFreeAbelianGroup.comp (Finsupp.singleAddHom x) = (smulAddHom ℤ (FreeAbelianGroup X)).flip (of x) :=
  AddMonoidHom.ext <| toFreeAbelianGroup_single _

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