Def RelIso.relIsoOfUniqueOfIrrefl

Modification history

2024-12-27 11:03

Mathlib/Order/RelIso/Basic.lean

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

Deleted RelIso.relIsoOfUniqueOfIrrefl View on Github →

2022-11-30 20:20

Mathlib/Order/RelIso/Basic.lean

feat: port Order.RelIso.Basic (#772) …

Added RelIso.relIsoOfUniqueOfIrrefl View on Github →