toFinsupp — Mathlib

English

There is a canonical group homomorphism from FreeAbelianGroup X to X →₀ ℤ, given by lifting an element to a finitely supported integer-valued function.

Русский

Существует канонический гомоморфизм группы от FreeAbelianGroup X к X →₀ ℤ, задаваемый логическим подъёмом элемента к конечной поддержке функции со значениями в ℤ.

LaTeX

$$toFinsupp : FreeAbelianGroup X →+ X →₀ ℤ$$

Lean4

/-- The group homomorphism `FreeAbelianGroup X →+ (X →₀ ℤ)`. -/
def toFinsupp : FreeAbelianGroup X →+ X →₀ ℤ :=
  FreeAbelianGroup.lift fun x => Finsupp.single x (1 : ℤ)

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