Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-29 14:28 70fcf999

View on Github →

feat(group_theory/free_abelian_group_finsupp): isomorphism between free_abelian_group and finsupp (#8046) From LTE

Estimated changes

Modified src/group_theory/free_abelian_group.lean

modified theorem free_abelian_group.map_of_apply

Created src/group_theory/free_abelian_group_finsupp.lean

added def finsupp.to_free_abelian_group

added theorem finsupp.to_free_abelian_group_comp_single_add_hom

added theorem finsupp.to_free_abelian_group_comp_to_finsupp

added theorem finsupp.to_free_abelian_group_to_finsupp

added def free_abelian_group.coeff

added def free_abelian_group.equiv_finsupp

added theorem free_abelian_group.mem_support_iff

added theorem free_abelian_group.not_mem_support_iff

added def free_abelian_group.support

added theorem free_abelian_group.support_add

added theorem free_abelian_group.support_gsmul

added theorem free_abelian_group.support_neg

added theorem free_abelian_group.support_nsmul

added theorem free_abelian_group.support_of

added theorem free_abelian_group.support_zero

added def free_abelian_group.to_finsupp

added theorem free_abelian_group.to_finsupp_comp_to_free_abelian_group

added theorem free_abelian_group.to_finsupp_of

added theorem free_abelian_group.to_finsupp_to_free_abelian_group