Theorem Mathlib.Meta.NormNum.isRat_zpow_pos

Modification history

2024-01-22 21:46
Mathlib/Tactic/NormNum/Pow.lean
feat: implement zpow norm_num extension (#9875)
Added Mathlib.Meta.NormNum.isRat_zpow_posView on Github →