Def RelIso.ofUniqueOfRefl

Modification history

2026-01-09 08:53

Mathlib/Order/RelIso/Basic.lean

chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)

Modified RelIso.ofUniqueOfRefl View on Github →

2024-12-27 11:03

Mathlib/Order/RelIso/Basic.lean

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

Added RelIso.ofUniqueOfRefl View on Github →