mathlib3 documentation

group_theory.free_abelian_group_finsupp

Isomorphism between free_abelian_group X and X →₀ ℤ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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
noncomputable def free_abelian_group.basis (α : Type u_1) :

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

Equations

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

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

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

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
@[simp]
@[simp]
theorem free_abelian_group.support_of {X : Type u_1} (x : X) :
@[simp]
@[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) :