Theorem ENNReal.iSup₂_pow_of_ne_zero

Modification history

2025-08-08 14:49
Mathlib/Topology/Instances/NNReal/Lemmas.lean
feat: add lemmas on `spectralRadius` along with supporting lemmas (#27993) …
Added ENNReal.iSup₂_pow_of_ne_zeroView on Github →