toFreeAbelianGroup_toFinsupp — Mathlib

English

The free abelian group on a type X is canonically isomorphic to the group of finitely supported integer-valued functions on X. The two natural maps toFinsupp and toFreeAbelianGroup are inverse to each other.

Русский

Свободная абелева группа на множество X естественным образом изоморфна группе конечносопровождаемых функций X → ℤ. Преобразования toFinsupp и toFreeAbelianGroup образуют взаимно обратные отображения.

LaTeX

$$$\\forall x \\in FreeAbelianGroup X,\; Finsupp.toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x$$$

Lean4

@[simp]
theorem toFreeAbelianGroup_toFinsupp {X} (x : FreeAbelianGroup X) :
    Finsupp.toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x := by
  rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]

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