mathlib
708d99aa - feat(data/real/ennreal): add `to_real_sub_of_le` (#8674)

Commit

4 years ago

feat(data/real/ennreal): add `to_real_sub_of_le` (#8674)

Author

kex-y

kex-y

Parents

Loading