Theorem NNReal.list_prod_map_rpow

Modification history

2023-08-09 15:56
Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
feat(Analysis/SpecialFunctions/Pow): powers of finite products (#6470)
Added NNReal.list_prod_map_rpowView on Github →