Commit 2022-07-28 17:47 39046bda

feat(data/{pi, prod}): add missing has_pow instances for pi type (#15478) This generalizes the existing powers by nat and int defined in later files to be defined for arbitrary powers. As well as eliminating the need for separate lemmas for these different power operations, this also means that tuples of real numbers now inherit a power operation by the real numbers.