Theorem NNReal.enorm_eq_coe

Modification history

2026-10-06 11:24
Mathlib/Analysis/Normed/Group/Real.lean
chore: extend L^p lemmas from normed spaces to enormed setting (#43834) …
Added NNReal.enorm_eq_coeView on Github →