Theorem toNNReal_enorm

Modification history

2026-02-09 11:06
Mathlib/Analysis/Normed/Group/Basic.lean
refactor(Analysis/Normed/Group): split large file (#34802) …
Modified toNNReal_enormView on Github →
2025-02-01 15:38
Mathlib/Analysis/Normed/Group/Basic.lean
feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) …
Added toNNReal_enormView on Github →