Def Mathlib.Tactic.Linarith.Expr.Ord

Modification history

2026-03-25 05:05
Mathlib/Tactic/Linarith/Preprocessing.lean
chore: remove declarations deprecated between 2021-03-24 and 2025-09-24 (#37118) …
Deleted Mathlib.Tactic.Linarith.Expr.OrdView on Github →
2025-06-19 05:18
Mathlib/Tactic/Linarith/Preprocessing.lean
chore(Tactic/Linarith): put linarith declarations into `Mathlib.Tactic` namespace (#25955) …
Added Mathlib.Tactic.Linarith.Expr.OrdView on Github →