Def FreeGroup.mulEquivIntOfUnique

Modification history

2026-03-16 19:13

Mathlib/GroupTheory/FreeGroup/Basic.lean

feat(GroupTheory/FreeGroup/Basic): deprecate `FreeGroup Empty ≃ Unit` using `Equiv.ofUnique`, add `Mul` suggestion using `MulEquiv.ofUnique` and add `FreeGroup α ≃* Multiplicative ℤ` (#34621) …

Added FreeGroup.mulEquivIntOfUnique View on Github →