Commit 2025-12-11 12:43 262b8863

View on Github →

chore: replace omega with lia where possible (#32666) As previously discussed, we'd like to move users off omega and on to lia (which is the linear integer arithmetic module from grind, plus a controlled set of instantiated lemmas). This does not yet remove all uses of omega in Mathlib.

Estimated changes