DiscriminantBounds
📁 Source: FLT/NumberField/DiscriminantBounds.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsrootDiscrBound | 1 |
| 7 | |
| Total | 8 |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
rootDiscrBound 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
le_five_of_rootDiscrBound 📖 | — | — | — | — | rootDiscrBound_lt_iff_lt_five |
le_fourteen_of_rootDiscrBound 📖 | — | rootDiscrBound | — | — | rootDiscrBound_lt_iff_lt_fourteen |
rootDiscrBound_lt_iff_lt_five 📖 | mathematical | — | rootDiscrBound | — | rootDiscrBound_strictMono |
rootDiscrBound_lt_iff_lt_fourteen 📖 | mathematical | — | rootDiscrBound | — | rootDiscrBound_strictMono |
rootDiscrBound_strictMono 📖 | mathematical | — | rootDiscrBound | — | — |
strictMonoOn_Ici_nat_of_lt_succ 📖 | — | — | — | — | — |
strictMonoOn_Ioi_nat_of_lt_succ 📖 | — | — | — | — | strictMonoOn_Ici_nat_of_lt_succ |
---