Theorem Mathlib.Meta.NormNum.isRat_rpow_pos

Modification history

2024-01-23 02:18
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
feat: implement rpow norm_num extension (#9893) …
Added Mathlib.Meta.NormNum.isRat_rpow_posView on Github →