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
Main declarations #
Isomorphic free ablian groups (as modules) have equivalent bases.
Isomorphic free abelian groups (as additive groups) have equivalent bases.
Isomorphic free groups have equivalent bases.
Isomorphic free groups have equivalent bases (
coeff x is the additive group homomorphism
free_abelian_group X →+ ℤ
a to the multiplicity of
x : X in
support a for
a : free_abelian_group X is the finite set of
x : X
that occur in the formal sum