Theorem Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow

Modification history

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