Theorem Sum.LiftRel.refl

Modification history

2026-01-09 08:53

Mathlib/Data/Sum/Order.lean

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

Modified Sum.LiftRel.refl View on Github →

2022-12-07 07:48

Mathlib/Data/Sum/Order.lean

feat port: Data.Sum.Order (#880) …

Added Sum.LiftRel.refl View on Github →