Commit 2024-11-22 22:03 9e7e4273

View on Github →

chore(Algebra/Order/SuccPred/TypeTags): fix defeq abuse with Additive and Multiplicative (#19379) these simp lemmas now don't use defeq abuse between A and Multiplicative A.

Estimated changes

modified theorem Order.pred_toAdd
modified theorem Order.pred_toMul
modified theorem Order.succ_toAdd
modified theorem Order.succ_toMul