Commit 2025-02-01 15:38 3d94db3c

View on Github →

feat: ‖x‖ₑ.toNNReal = ‖x‖₊ (#21306) From LeanAPAP

Estimated changes

added theorem toNNReal_enorm