toFinsupp_toFreeAbelianGroup — Mathlib

English

For every finitely supported function f: X → ℤ, applying toFreeAbelianGroup after toFinsupp returns the original function; i.e., the two conversions are inverses on Finsupp.

Русский

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

LaTeX

$$$\\forall f : X \\to_{0} \\mathbb{Z},\\ FreeAbelianGroup.toFinsupp (Finsupp.toFreeAbelianGroup f) = f$$$

Lean4

@[simp]
theorem toFinsupp_toFreeAbelianGroup (f : X →₀ ℤ) : FreeAbelianGroup.toFinsupp (Finsupp.toFreeAbelianGroup f) = f := by
  rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]

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