ennreal): Positivity extension for `ennreal.of_real` (#16955)

Commit

3 years ago

feat(data/real/ennreal): Positivity extension for `ennreal.of_real` (#16955) and three easy lemmas

Author

YaelDillies

Parents