Theorem Mathlib.Meta.NormNum.rpow_isRat_eq_inv_rpow

Modification history

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