mathlib
50a4565f - feat(order/basic): Product of dense orders (#17168)

Commit

3 years ago

feat(order/basic): Product of dense orders (#17168) The (arbitrary) product of dense orders is dense.

Author

YaelDillies

Parents