# Documentation

Mathlib.GroupTheory.FreeAbelianGroupFinsupp

# Isomorphism between FreeAbelianGroup X and X →₀ ℤ#

In this file we construct the canonical isomorphism between FreeAbelianGroup X and X →₀ ℤ. We use this to transport the notion of support from Finsupp to FreeAbelianGroup.

## Main declarations #

• FreeAbelianGroup.equivFinsupp: group isomorphism between FreeAbelianGroup X and X →₀ ℤ
• FreeAbelianGroup.coeff: the multiplicity of x : X in a : FreeAbelianGroup X
• FreeAbelianGroup.support: the finset of x : X that occur in a : FreeAbelianGroup X

The group homomorphism FreeAbelianGroup X →+ (X →₀ ℤ).

Instances For

The group homomorphism (X →₀ ℤ) →+ FreeAbelianGroup X.

Instances For
@[simp]
theorem Finsupp.toFreeAbelianGroup_comp_singleAddHom {X : Type u_1} (x : X) :
AddMonoidHom.comp Finsupp.toFreeAbelianGroup () = ↑() ()
@[simp]
theorem FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup {X : Type u_1} :
@[simp]
theorem Finsupp.toFreeAbelianGroup_comp_toFinsupp {X : Type u_1} :
@[simp]
theorem Finsupp.toFreeAbelianGroup_toFinsupp {X : Type u_2} (x : ) :
Finsupp.toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x
@[simp]
theorem FreeAbelianGroup.toFinsupp_of {X : Type u_1} (x : X) :
FreeAbelianGroup.toFinsupp () = fun₀ | x => 1
@[simp]
theorem FreeAbelianGroup.toFinsupp_toFreeAbelianGroup {X : Type u_1} (f : X →₀ ) :
FreeAbelianGroup.toFinsupp (Finsupp.toFreeAbelianGroup f) = f
@[simp]
theorem FreeAbelianGroup.equivFinsupp_apply (X : Type u_1) (a : ) :
= FreeAbelianGroup.toFinsupp a
@[simp]
theorem FreeAbelianGroup.equivFinsupp_symm_apply (X : Type u_1) (a : X →₀ ) :
= Finsupp.toFreeAbelianGroup a

The additive equivalence between FreeAbelianGroup X and (X →₀ ℤ).

Instances For
noncomputable def FreeAbelianGroup.basis (α : Type u_2) :

A is a basis of the ℤ-module FreeAbelianGroup A.

Instances For
def FreeAbelianGroup.Equiv.ofFreeAbelianGroupLinearEquiv {α : Type u_2} {β : Type u_3} (e : ) :
α β

Isomorphic free abelian groups (as modules) have equivalent bases.

Instances For
def FreeAbelianGroup.Equiv.ofFreeAbelianGroupEquiv {α : Type u_2} {β : Type u_3} (e : ) :
α β

Isomorphic free abelian groups (as additive groups) have equivalent bases.

Instances For
def FreeAbelianGroup.Equiv.ofFreeGroupEquiv {α : Type u_2} {β : Type u_3} (e : ) :
α β

Isomorphic free groups have equivalent bases.

Instances For
def FreeAbelianGroup.Equiv.ofIsFreeGroupEquiv {G : Type u_2} {H : Type u_3} [] [] [] [] (e : G ≃* H) :

Isomorphic free groups have equivalent bases (IsFreeGroup variant).

Instances For
def FreeAbelianGroup.coeff {X : Type u_1} (x : X) :

coeff x is the additive group homomorphism FreeAbelianGroup X →+ ℤ that sends a to the multiplicity of x : X in a.

Instances For
def FreeAbelianGroup.support {X : Type u_1} (a : ) :

support a for a : FreeAbelianGroup X is the finite set of x : X that occur in the formal sum a.

Instances For
theorem FreeAbelianGroup.mem_support_iff {X : Type u_1} (x : X) (a : ) :
↑() a 0
theorem FreeAbelianGroup.not_mem_support_iff {X : Type u_1} (x : X) (a : ) :
↑() a = 0
@[simp]
@[simp]
theorem FreeAbelianGroup.support_of {X : Type u_1} (x : X) :
@[simp]
theorem FreeAbelianGroup.support_neg {X : Type u_1} (a : ) :
@[simp]
theorem FreeAbelianGroup.support_zsmul {X : Type u_1} (k : ) (h : k 0) (a : ) :
@[simp]
theorem FreeAbelianGroup.support_nsmul {X : Type u_1} (k : ) (h : k 0) (a : ) :
theorem FreeAbelianGroup.support_add {X : Type u_1} (a : ) (b : ) :