Def Tactic.NormNum.evalIrrationalRpow

Modification history

2026-07-16 01:47
Mathlib/Tactic/NormNum/Irrational.lean
chore: bump toolchain to v4.33.0-rc1 (#41779)
Deleted Tactic.NormNum.evalIrrationalRpowView on Github →
2026-06-18 23:59
Mathlib/Tactic/NormNum/Irrational.lean
chore: bump toolchain to v4.32.0-rc1 (#40732)
Modified Tactic.NormNum.evalIrrationalRpowView on Github →
2025-05-22 13:29
Mathlib/Tactic/NormNum/Irrational.lean
feat(Tactic/NormNum): `norm_num` extension for `Irrational x^y` (#22794) …
Added Tactic.NormNum.evalIrrationalRpowView on Github →