Theorem Order.pred_ofMul

Modification history

2024-09-16 17:23

Mathlib/Algebra/Order/SuccPred/TypeTags.lean

feat(Order/SuccPred/TypeTags): `SuccOrder (Multiplicative X)` and friends (#15940)

Added Order.pred_ofMul View on Github →