Commit 2023-08-09 15:56 9f2c0782

View on Github →

feat(Analysis/SpecialFunctions/Pow): powers of finite products (#6470)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

added theorem NNReal.finset_prod_rpow

added theorem NNReal.list_prod_map_rpow'

added theorem NNReal.list_prod_map_rpow

added theorem NNReal.multiset_prod_map_rpow

added def NNReal.rpowMonoidHom

added theorem Real.finset_prod_rpow

added theorem Real.list_prod_map_rpow'

added theorem Real.list_prod_map_rpow

added theorem Real.multiset_prod_map_rpow

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean