mathlib3
9da39cf9 - feat(ordered_field): missing inequality lemmas (#4090)

Commit

5 years ago

feat(ordered_field): missing inequality lemmas (#4090) From the sphere eversion project.

References

Author

PatrickMassot

Parents