Core
📁 Source: Mathlib/Tactic/Nontriviality/Core.lean
Statistics
| Metric | Count |
|---|---|
| 3 | |
Theoremssubsingleton_or_nontrivial_elim | 1 |
| Total | 4 |
Mathlib.Tactic.Nontriviality
Definitions
| Name | Category | Theorems |
|---|---|---|
elabNontriviality 📖 | CompOp | — |
nontrivialityByAssumption 📖 | CompOp | — |
nontrivialityByElim 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
subsingleton_or_nontrivial_elim 📖 | — | — | — | — | subsingleton_or_nontrivial |
---