Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-06 22:54 7c53a168

View on Github →

feat(algebra/ordered_ring): add lemma (#6031) Add a lemma in algebra.ordered_ring proving the inequality a + (2 + b) ≤ a * (2 + b). This is again part of the Liouville PR.

Estimated changes