mathlib

7c53a168 - feat(algebra/ordered_ring): add lemma (#6031)

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.