Theorem Order.IsNormal.of_succ_lt

Modification history

2025-08-20 12:55
Mathlib/Order/IsNormal.lean
feat: extensionality for normal functions (#28677) …
Modified Order.IsNormal.of_succ_ltView on Github →
2025-04-03 11:14
Mathlib/Order/IsNormal.lean
feat: generalize normal functions (#20504) …
Added Order.IsNormal.of_succ_ltView on Github →