Commit 2025-05-22 13:29 fabf7ef1

View on Github →

feat(Tactic/NormNum): norm_num extension for Irrational x^y (#22794) Add norm_num extension for Irrational x^y.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/NormNum/Irrational.lean

added structure Tactic.NormNum.NotPowerCertificate

added def Tactic.NormNum.evalIrrationalRpow

added def Tactic.NormNum.evalIrrationalSqrt

added def Tactic.NormNum.findNotPowerCertificate

added def Tactic.NormNum.findNotPowerCertificateCore

Modified MathlibTest/norm_num_ext.lean