Structure Tactic.NormNum.NotPowerCertificate

Modification history

2026-07-16 01:47
Mathlib/Tactic/NormNum/Irrational.lean
chore: bump toolchain to v4.33.0-rc1 (#41779)
Deleted Tactic.NormNum.NotPowerCertificateView 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.NotPowerCertificateView on Github →