Commit 2021-06-22 08:42 faaa0bcb
View on Github →feat(algebra/ordered_field): (1 - 1 / a)⁻¹ ≤ 2 (#8021)
A lemma from the Liouville PR #8001. I extracted this lemma, after the discussion there.
feat(algebra/ordered_field): (1 - 1 / a)⁻¹ ≤ 2 (#8021)
A lemma from the Liouville PR #8001. I extracted this lemma, after the discussion there.