Def Nat.disjointedRec

Modification history

2025-01-21 20:44

Mathlib/Algebra/Order/Disjointed.lean

refactor(Order/Disjointed): allow arbitrary partial orders as domain (#20545)

Added Nat.disjointedRec View on Github →