equivFinsupp — Mathlib

English

There is a canonical additive equivalence between FreeAbelianGroup X and X →₀ ℤ, giving an explicit isomorphism between the two structures that preserves addition.

Русский

Существует каноническое добавное эквивалентство между FreeAbelianGroup X и X →₀ ℤ, задающее явное изоморфное соответствие между двумя структурами и сохраняющее сложение.

LaTeX

$$$FreeAbelianGroup X \\cong_{+} (X \\to_{0} \\mathbb{Z})$$$

Lean4

/-- The additive equivalence between `FreeAbelianGroup X` and `(X →₀ ℤ)`. -/
@[simps!]
def equivFinsupp : FreeAbelianGroup X ≃+ (X →₀ ℤ)
    where
  toFun := toFinsupp
  invFun := toFreeAbelianGroup
  left_inv := toFreeAbelianGroup_toFinsupp
  right_inv := toFinsupp_toFreeAbelianGroup
  map_add' := toFinsupp.map_add

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