mathlib

a44ce4da - feat(real/ennreal): basic lemmas about `ennreal.to_nnreal` and `ennreal.to_real` (#16318)

feat(real/ennreal): basic lemmas about `ennreal.to_nnreal` and `ennreal.to_real` (#16318) Provides lemmas for when `to_nnreal` or `to_real` equal `1`, and when two instances of `to_nnreal` and `to_real` equal each other.