Theorem AntisymmRel.of_eq

Modification history

2026-01-09 08:53
Mathlib/Order/Antisymmetrization.lean
chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)
Modified AntisymmRel.of_eqView on Github →
2025-03-01 11:50
Mathlib/Order/Antisymmetrization.lean
feat: `a = b → AntisymmRel r a b` (#22268)
Added AntisymmRel.of_eqView on Github →