mathlib documentation

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 #

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

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