Theorem irrefl_def

Modification history

2026-04-14 12:34

Mathlib/Order/Defs/Unbundled.lean

chore(Order/Defs/Unbundled): deprecate `def Reflexive` in favor of `class Std.Refl` (#37278) …

Added irrefl_def View on Github →