Commit 2025-07-13 19:58 27ba7f0e

View on Github →

feat: FreeAbelianGroup.lift as an equivalence of groups (#27032) From Toric

Estimated changes

Modified Mathlib/GroupTheory/FreeAbelianGroup.lean

deleted theorem FreeAbelianGroup.lift.add'

added def FreeAbelianGroup.liftAddEquiv

added theorem FreeAbelianGroup.lift_add

added theorem FreeAbelianGroup.lift_add_apply

deleted theorem FreeAbelianGroup.lift_neg'

added theorem FreeAbelianGroup.lift_neg

added theorem FreeAbelianGroup.lift_neg_apply

modified def FreeAbelianGroup.seqAddGroupHom

Modified scripts/nolints_prime_decls.txt