# mathlibdocumentation

group_theory.free_abelian_group_finsupp

# Isomorphism between free_abelian_group X and X →₀ ℤ#

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

## Main declarations #

• free_abelian_group.equiv_finsupp: group isomorphism between free_abelian_group X and X →₀ ℤ
• free_abelian_group.coeff: the multiplicity of x : X in a : free_abelian_group X
• free_abelian_group.support: the finset of x : X that occur in a : free_abelian_group X
noncomputable def free_abelian_group.to_finsupp {X : Type u_1} :

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

Equations
noncomputable def finsupp.to_free_abelian_group {X : Type u_1} :

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

Equations
@[simp]
theorem finsupp.to_free_abelian_group_comp_single_add_hom {X : Type u_1} (x : X) :
@[simp]
@[simp]
@[simp]
@[simp]
theorem free_abelian_group.to_finsupp_of {X : Type u_1} (x : X) :
@[simp]
@[simp]
theorem free_abelian_group.equiv_finsupp_apply (X : Type u_1) (ᾰ : free_abelian_group X) :
noncomputable def free_abelian_group.equiv_finsupp (X : Type u_1) :

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

Equations
@[simp]
theorem free_abelian_group.equiv_finsupp_symm_apply (X : Type u_1) (ᾰ : X →₀ ) :
noncomputable def free_abelian_group.basis (α : Type u_1) :

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

Equations
noncomputable def free_abelian_group.equiv.of_free_abelian_group_linear_equiv {α : Type u_1} {β : Type u_2}  :
α β

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

Equations
• = let t : := in
noncomputable def free_abelian_group.equiv.of_free_abelian_group_equiv {α : Type u_1} {β : Type u_2}  :
α β

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

Equations
noncomputable def free_abelian_group.equiv.of_free_group_equiv {α : Type u_1} {β : Type u_2} (e : ≃* ) :
α β

Isomorphic free groups have equivalent bases.

Equations
noncomputable def free_abelian_group.equiv.of_is_free_group_equiv {G : Type u_1} {H : Type u_2} [group G] [group H] (e : G ≃* H) :

Isomorphic free groups have equivalent bases (is_free_group variant).

Equations
noncomputable def free_abelian_group.coeff {X : Type u_1} (x : X) :

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

Equations
noncomputable def free_abelian_group.support {X : Type u_1} (a : free_abelian_group X) :

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

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