Commit 2024-01-23 02:18 80500592

feat: implement rpow norm_num extension (#9893)

• Implements a norm_num extension for a ^ b where a and b are reals. Unlike in the mathlib3 version, there is no restriction on the positivity of a.
• Moves commented-out tests from test/norm_num_ext.lean into a new file test/norm_num_rpow.lean, to keep the dependencies of norm_num_ext.lean lightweight.