push
📁 Source: MathlibTest/push.lean
Statistics
| Metric | Count |
|---|---|
| 2 | |
Theoremspush | 1 |
| Total | 3 |
Lean.Meta.RefinedDiscrTree.PreDiscrTree
Definitions
| Name | Category | Theorems |
|---|---|---|
push 📖 | CompOp | — |
Mathlib.Tactic.Push
Definitions
| Name | Category | Theorems |
|---|---|---|
push 📖 | CompOp | — |
Tactic.ComputeAsymptotics.WellFormedBasis
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
push 📖 | mathematical | Tactic.ComputeAsymptotics.WellFormedBasisFilter.TendstoRealFilter.atTopReal.instPreorderAsymptotics.IsLittleOReal.normReal.log | Tactic.ComputeAsymptotics.Basis | — | insertinstIsEmptyFalse |
---