Irrational

📁 Source: Mathlib/Tactic/NormNum/Irrational.lean

Statistics

Metric	Count
Definitions NotPowerCertificate, k, pf_left, pf_right, evalIrrationalRpow, evalIrrationalSqrt, findNotPowerCertificate, findNotPowerCertificateCore	8
Theorems	0
Total	8

Tactic.NormNum

Definitions

Name	Category	Theorems
NotPowerCertificate 📖	CompData	—
evalIrrationalRpow 📖	CompOp	—
evalIrrationalSqrt 📖	CompOp	—
findNotPowerCertificate 📖	CompOp	—
findNotPowerCertificateCore 📖	CompOp	—

Tactic.NormNum.NotPowerCertificate

Definitions

Name	Category	Theorems
k 📖	CompOp	—
pf_left 📖	CompOp	—
pf_right 📖	CompOp	—

---

← Back to Index