FieldSimp
📁 Source: Mathlib/Tactic/FieldSimp.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsDenomCondition, proof, proofZero, convField_simp__, fieldSimp, mkDenomConditionProofSucc, mkDenomConditionProofSucc', normalize, parseDischarger, proc, qNF, div, evalPretty, evalPrettyMonomial, gcd, mkDivProof, mkMulProof, mul, onExponent, removeZeros, split, toNF, tryClearZero, reduceEqQ, reduceExpr, reduceExprQ, reduceLeQ, reduceLtQ, reduceProp, fieldEq, fieldLe, fieldLt | 32 |
| Theorems | 0 |
| Total | 32 |
Mathlib.Tactic.FieldSimp
Definitions
| Name | Category | Theorems |
|---|---|---|
DenomCondition 📖 | CompData | — |
convField_simp__ 📖 | CompOp | — |
fieldSimp 📖 | CompOp | — |
mkDenomConditionProofSucc 📖 | CompOp | — |
mkDenomConditionProofSucc' 📖 | CompOp | — |
normalize 📖 | CompOp | — |
parseDischarger 📖 | CompOp | — |
proc 📖 | CompOp | — |
qNF 📖 | CompOp | — |
reduceEqQ 📖 | CompOp | — |
reduceExpr 📖 | CompOp | — |
reduceExprQ 📖 | CompOp | — |
reduceLeQ 📖 | CompOp | — |
reduceLtQ 📖 | CompOp | — |
reduceProp 📖 | CompOp | — |
Mathlib.Tactic.FieldSimp.DenomCondition
Definitions
| Name | Category | Theorems |
|---|---|---|
proof 📖 | CompOp | — |
proofZero 📖 | CompOp | — |
Mathlib.Tactic.FieldSimp.qNF
Definitions
| Name | Category | Theorems |
|---|---|---|
div 📖 | CompOp | — |
evalPretty 📖 | CompOp | — |
evalPrettyMonomial 📖 | CompOp | — |
gcd 📖 | CompOp | — |
mkDivProof 📖 | CompOp | — |
mkMulProof 📖 | CompOp | — |
mul 📖 | CompOp | — |
onExponent 📖 | CompOp | — |
removeZeros 📖 | CompOp | — |
split 📖 | CompOp | — |
toNF 📖 | CompOp | — |
tryClearZero 📖 | CompOp | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
fieldEq 📖 | CompOp | — |
fieldLe 📖 | CompOp | — |
fieldLt 📖 | CompOp | — |
---