Def RelIso.ofUniqueOfIrrefl

Modification history

2024-12-27 11:03
Mathlib/Order/RelIso/Basic.lean
chore: rename `MulEquiv.mulEquivOfUnique` to `MulEquiv.ofUnique` (#20243)
Added RelIso.ofUniqueOfIrreflView on Github →