Commit 2026-03-16 19:13 a04c5481

feat(GroupTheory/FreeGroup/Basic): deprecate FreeGroup Empty ≃ Unit using Equiv.ofUnique, add Mul suggestion using MulEquiv.ofUnique and add FreeGroup α ≃* Multiplicative ℤ (#34621) feat(GroupTheory/FreeGroup/Basic): deprecate FreeGroup Empty ≃ Unit using Equiv.ofUnique, add Mul suggestion using MulEquiv.ofUnique and add FreeGroup α ≃* Multiplicative ℤ. This is a dependency of a larger PR to formalize finitely presented groups https://github.com/leanprover-community/mathlib4/pull/34236.