mathlib
b3943dc0 - feat(algebra/archimedean): `order_dual α` is archimedean (#8476)

Commit

4 years ago

feat(algebra/archimedean): `order_dual α` is archimedean (#8476)

Author

urkud

urkud

Parents

Loading