Commit 2024-01-22 21:46 5a0540a5

View on Github →

feat: implement zpow norm_num extension (#9875)

Estimated changes

Modified Mathlib/Tactic/NormNum/Pow.lean

added def Mathlib.Meta.NormNum.evalZPow

added theorem Mathlib.Meta.NormNum.isInt_zpow_neg

added theorem Mathlib.Meta.NormNum.isInt_zpow_pos

added theorem Mathlib.Meta.NormNum.isNat_zpow_neg

added theorem Mathlib.Meta.NormNum.isNat_zpow_pos

added theorem Mathlib.Meta.NormNum.isRat_zpow_neg

added theorem Mathlib.Meta.NormNum.isRat_zpow_pos

Modified test/norm_num.lean