Commit 2025-07-23 20:45 5efaaa73

View on Github →

chore: rename lift.of to lift_apply_of (#27398)

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Adjunctions.lean

Modified Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean

Modified Mathlib/GroupTheory/Abelianization/Defs.lean

deleted theorem Abelianization.lift.of

deleted theorem Abelianization.lift.unique

added theorem Abelianization.lift_apply_of

added theorem Abelianization.lift_unique

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/GroupTheory/FreeAbelianGroup.lean

modified theorem FreeAbelianGroup.lift.map_hom

added theorem FreeAbelianGroup.lift_apply_of

added theorem FreeAbelianGroup.lift_comp_apply

added theorem FreeAbelianGroup.lift_ext

added theorem FreeAbelianGroup.lift_unique

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

deleted theorem FreeGroup.lift.mk

deleted theorem FreeGroup.lift.of

deleted theorem FreeGroup.lift.of_eq

deleted theorem FreeGroup.lift.range_eq_closure

deleted theorem FreeGroup.lift.range_le

deleted theorem FreeGroup.lift.unique

added theorem FreeGroup.lift_apply_of

added theorem FreeGroup.lift_mk

added theorem FreeGroup.lift_of_apply

added theorem FreeGroup.lift_unique

added theorem FreeGroup.range_lift_eq_closure

added theorem FreeGroup.range_lift_le

Modified Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean

Modified Mathlib/GroupTheory/PresentedGroup.lean

Modified Mathlib/RingTheory/FreeCommRing.lean