NeZero
📁 Source: Mathlib/Algebra/NeZero.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 14 | |
| Total | 14 |
NeZero
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
of_pos 📖 | — | Preorder.toLT | — | — | ne_of_gt |
(root)
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
eq_zero_or_neZero 📖 | — | — | — | — | eq_or_ne |
four_ne_zero 📖 | — | — | — | — | — |
four_ne_zero' 📖 | — | — | — | — | four_ne_zero |
ne_zero_of_eq_one 📖 | — | — | — | — | one_ne_zero |
not_neZero 📖 | — | — | — | — | — |
one_ne_zero 📖 | — | — | — | — | — |
one_ne_zero' 📖 | — | — | — | — | one_ne_zero |
three_ne_zero 📖 | — | — | — | — | — |
three_ne_zero' 📖 | — | — | — | — | three_ne_zero |
two_ne_zero 📖 | — | — | — | — | — |
two_ne_zero' 📖 | — | — | — | — | two_ne_zero |
zero_ne_one 📖 | — | — | — | — | — |
zero_ne_one' 📖 | — | — | — | — | zero_ne_one |
---