Theorem NNReal.multiset_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.multiset_prod_map_rpow View on Github →