Documentation Verification Report

Verification

📁 Source: Mathlib/Tactic/Linarith/Verification.lean

Statistics

MetricCount
DefinitionsaddExprs, addExprs', addIneq, addNegEqProofsIdx, leftOfIneqProof, mkLTZeroProof, mkNegOneLtZeroProof, mulExpr, mulExpr', proveEqZeroUsing, proveFalseByLinarith, typeOfIneqProof, ofNatQ
13
Theorems0
Total13

Mathlib.Tactic.Linarith

Definitions

NameCategoryTheorems
addExprs 📖CompOp—
addExprs' 📖CompOp—
addIneq 📖CompOp—
addNegEqProofsIdx 📖CompOp—
leftOfIneqProof 📖CompOp—
mkLTZeroProof 📖CompOp—
mkNegOneLtZeroProof 📖CompOp—
mulExpr 📖CompOp—
mulExpr' 📖CompOp—
proveEqZeroUsing 📖CompOp—
proveFalseByLinarith 📖CompOp—
typeOfIneqProof 📖CompOp—

Qq

Definitions

NameCategoryTheorems
ofNatQ 📖CompOp—

---

← Back to Index