Theorem Abelianization.lift.unique

Modification history

2025-07-23 20:45

Mathlib/GroupTheory/Abelianization/Defs.lean

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

Deleted Abelianization.lift.unique View on Github →

2025-07-23 15:29

Mathlib/GroupTheory/Abelianization.lean

chore(GroupTheory/FreeAbelianGroup): do not import cardinals (#27169) …

Modified Abelianization.lift.unique View on Github →

2023-02-11 21:40

Mathlib/GroupTheory/Abelianization.lean

feat: port GroupTheory.Abelianization (#2215)

Added Abelianization.lift.unique View on Github →