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.equivIntOfUnique