Theorem Mathlib.Meta.NormNum.isRat_rpow_pos

Modification history

2026-05-17 20:27
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted Mathlib.Meta.NormNum.isRat_rpow_posView on Github →
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 →