Theorem Order.pred_toMul

Modification history

2025-07-25 21:58
Mathlib/Algebra/Order/SuccPred/TypeTags.lean
chore: fix more indentation (#27491) …
Modified Order.pred_toMulView on Github →
2024-11-22 22:03
Mathlib/Algebra/Order/SuccPred/TypeTags.lean
chore(Algebra/Order/SuccPred/TypeTags): fix defeq abuse with Additive and Multiplicative (#19379) …
Modified Order.pred_toMulView on Github →
2024-09-16 17:23
Mathlib/Algebra/Order/SuccPred/TypeTags.lean
feat(Order/SuccPred/TypeTags): `SuccOrder (Multiplicative X)` and friends (#15940)
Added Order.pred_toMulView on Github →