Commit 2023-04-17 07:18 0a4bbecc

View on Github →

feat: port GroupTheory.FreeAbelianGroupFinsupp (#3441)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/GroupTheory/FreeAbelianGroup.lean

Created Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean

added def Finsupp.toFreeAbelianGroup

added theorem Finsupp.toFreeAbelianGroup_comp_singleAddHom

added theorem Finsupp.toFreeAbelianGroup_comp_toFinsupp

added theorem Finsupp.toFreeAbelianGroup_toFinsupp

added def FreeAbelianGroup.Equiv.ofFreeAbelianGroupEquiv

added def FreeAbelianGroup.Equiv.ofFreeAbelianGroupLinearEquiv

added def FreeAbelianGroup.Equiv.ofFreeGroupEquiv

added def FreeAbelianGroup.Equiv.ofIsFreeGroupEquiv

added def FreeAbelianGroup.coeff

added def FreeAbelianGroup.equivFinsupp

added theorem FreeAbelianGroup.mem_support_iff

added theorem FreeAbelianGroup.not_mem_support_iff

added def FreeAbelianGroup.support

added theorem FreeAbelianGroup.support_add

added theorem FreeAbelianGroup.support_neg

added theorem FreeAbelianGroup.support_nsmul

added theorem FreeAbelianGroup.support_of

added theorem FreeAbelianGroup.support_zero

added theorem FreeAbelianGroup.support_zsmul

added def FreeAbelianGroup.toFinsupp

added theorem FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup

added theorem FreeAbelianGroup.toFinsupp_of

added theorem FreeAbelianGroup.toFinsupp_toFreeAbelianGroup