Adic
📁 Source: ClassFieldTheory/IsNonarchimedeanLocalField/Adic.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 3 | |
| Total | 3 |
IsNonarchimedeanLocalField
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
instIsAdicCompleteSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory 📖 | — | — | — | — | isAdicinstT2Space_classFieldTheory |
isAdic 📖 | — | — | — | — | maximalIdeal_pow_eq |
maximalIdeal_pow_eq 📖 | — | — | — | — | valuation_irreducible |
---