Theorem Real.toNNReal_zpow

Modification history

2025-04-02 09:26
Mathlib/Data/NNReal/Defs.lean
feat: a few lemmas from the Carleson project (#23545)
Added Real.toNNReal_zpowView on Github →