Commit 2023-03-14 11:44 0eb23819

View on Github →

feat: port GroupTheory.FreeAbelianGroup (#2247)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/FreeAbelianGroup.lean

added theorem FreeAbelianGroup.add_bind

added theorem FreeAbelianGroup.add_seq

added def FreeAbelianGroup.equivOfEquiv

added theorem FreeAbelianGroup.lift.add'

added theorem FreeAbelianGroup.lift.map_hom

added def FreeAbelianGroup.lift

added def FreeAbelianGroup.liftAddGroupHom

added def FreeAbelianGroup.liftMonoid

added theorem FreeAbelianGroup.liftMonoid_coe

added theorem FreeAbelianGroup.liftMonoid_coe_addMonoidHom

added theorem FreeAbelianGroup.liftMonoid_symm_coe

added theorem FreeAbelianGroup.lift_comp

added theorem FreeAbelianGroup.lift_neg'

added def FreeAbelianGroup.map

added theorem FreeAbelianGroup.map_comp

added theorem FreeAbelianGroup.map_comp_apply

added theorem FreeAbelianGroup.map_id

added theorem FreeAbelianGroup.map_id_apply

added theorem FreeAbelianGroup.map_of

added theorem FreeAbelianGroup.map_of_apply

added theorem FreeAbelianGroup.map_pure

added theorem FreeAbelianGroup.mul_def

added theorem FreeAbelianGroup.neg_bind

added theorem FreeAbelianGroup.neg_seq

added def FreeAbelianGroup.of

added def FreeAbelianGroup.ofMulHom

added theorem FreeAbelianGroup.ofMulHom_coe

added theorem FreeAbelianGroup.of_injective

added theorem FreeAbelianGroup.of_mul

added theorem FreeAbelianGroup.of_mul_of

added theorem FreeAbelianGroup.of_one

added theorem FreeAbelianGroup.one_def

added def FreeAbelianGroup.punitEquiv

added theorem FreeAbelianGroup.pure_bind

added theorem FreeAbelianGroup.pure_seq

added def FreeAbelianGroup.seqAddGroupHom

added theorem FreeAbelianGroup.seq_add

added theorem FreeAbelianGroup.seq_neg

added theorem FreeAbelianGroup.seq_sub

added theorem FreeAbelianGroup.seq_zero

added theorem FreeAbelianGroup.sub_bind

added theorem FreeAbelianGroup.sub_seq

added theorem FreeAbelianGroup.zero_bind

added theorem FreeAbelianGroup.zero_seq

added def FreeAbelianGroup