Commit 2025-03-20 20:33 158ebce4

View on Github →

chore(ENNReal): fix names (#23135) The names were suffixing _toReal/_toENNReal instead of prefixing them.

Estimated changes

deleted theorem ENNReal.one_toNNReal
deleted theorem ENNReal.one_toReal
added theorem ENNReal.toNNReal_one
added theorem ENNReal.toNNReal_top
added theorem ENNReal.toNNReal_zero
added theorem ENNReal.toReal_one
added theorem ENNReal.toReal_top
added theorem ENNReal.toReal_zero
deleted theorem ENNReal.top_toNNReal
deleted theorem ENNReal.top_toReal
deleted theorem ENNReal.zero_toNNReal
deleted theorem ENNReal.zero_toReal