Def MulEquiv.ofUnique

Modification history

2024-12-27 11:03

Mathlib/Algebra/Group/Equiv/Basic.lean

chore: rename `MulEquiv.mulEquivOfUnique` to `MulEquiv.ofUnique` (#20243)

Added MulEquiv.ofUnique View on Github →