mathlib

39046bda - feat(data/{pi, prod}): add missing `has_pow` instances for `pi` type (#15478)

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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>