Theorem Mathlib.Meta.NormNum.IsNat.rpow_isNNRat

Modification history

2025-10-23 12:28
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
feat: better `norm_num` for `rpow` (#30615) …
Added Mathlib.Meta.NormNum.IsNat.rpow_isNNRatView on Github →