a)⁻¹ ≤ 2` (#8021)

Commit

4 years ago

feat(algebra/ordered_field): `(1 - 1 / a)⁻¹ ≤ 2` (#8021) A lemma from the Liouville PR #8001. I extracted this lemma, after the discussion there.

Author

adomani

Parents