Commit 2025-10-23 12:28 c1927234

feat: better norm_num for rpow (#30615)

• Use recently added Nat.nthRoot to make (a : ℝ) ^ (b : ℝ) work for rational a ≥ 0 and b.
• Simplify the logic by using .eqTrans.