Documentation Verification Report

RamificationInertia

📁 Source: ClassFieldTheory/IsNonarchimedeanLocalField/RamificationInertia.lean

Statistics

Metric	Count
Definitions	0
Theorems `intermediateField`, `comap`, `n_dvd_f`, `n_eq_f`, `ofAlgEquiv`, `of_tower_bot`, `of_tower_top`, `trans`, `e_congr`, `e_dvd_e`, `e_dvd_e_bot`, `e_dvd_e_top`, `e_fieldRange`, `e_mul_e`, `f_congr`, `f_dvd_f`, `f_dvd_f_bot`, `f_dvd_f_top`, `f_fieldRange`, `f_mul_f`, `instIsScalarTowerResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_2`, `instIsUnramifiedSubtypeMemIntermediateFieldFieldRange`	23
Total	23

IsNonarchimedeanLocalField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`e_congr` 📖	mathematical	—	`e`	—	`e_dvd_e`
`e_dvd_e` 📖	mathematical	—	`e`	—	`of_tower_top` `e_dvd_e_top`
`e_dvd_e_bot` 📖	mathematical	—	`e`	—	`e_mul_e`
`e_dvd_e_top` 📖	mathematical	—	`e`	—	`e_mul_e`
`e_fieldRange` 📖	mathematical	—	`e` `ValuativeRel.instSubtypeMem_classFieldTheory` `instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1`	—	`e_congr` `instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1`
`e_mul_e` 📖	mathematical	—	`e`	—	`f_pos` `e_mul_f_eq_n` `f_mul_f` `instFiniteDimensional_classFieldTheory`
`f_congr` 📖	mathematical	—	`f`	—	`f_dvd_f`
`f_dvd_f` 📖	mathematical	—	`f`	—	`of_tower_top` `f_dvd_f_top`
`f_dvd_f_bot` 📖	mathematical	—	`f`	—	`f_mul_f`
`f_dvd_f_top` 📖	mathematical	—	`f`	—	`f_mul_f`
`f_fieldRange` 📖	mathematical	—	`f` `ValuativeRel.instSubtypeMem_classFieldTheory` `instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1`	—	`f_congr` `instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1`
`f_mul_f` 📖	mathematical	—	`f`	—	`instIsScalarTowerResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `instFiniteDimensionalResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`instIsScalarTowerResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	mathematical	—	`instAlgebraResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_2`
`instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_2` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	—
`instIsUnramifiedSubtypeMemIntermediateFieldFieldRange` 📖	mathematical	—	`IsUnramified` `ValuativeRel.instSubtypeMem_classFieldTheory` `instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1`	—	`instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1` `e_fieldRange` `IsUnramified.e_eq_one`

IsNonarchimedeanLocalField.InUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intermediateField` 📖	mathematical	—	`IsNonarchimedeanLocalField.IsUnramified` `ValuativeRel.instSubtypeMem_classFieldTheory` `IsNonarchimedeanLocalField.instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1`	—	`IsNonarchimedeanLocalField.instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1` `IsNonarchimedeanLocalField.e_dvd_e` `IsNonarchimedeanLocalField.IsUnramified.e_eq_one`

IsNonarchimedeanLocalField.IsUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	—	`IsNonarchimedeanLocalField.IsUnramified`	—	`IsNonarchimedeanLocalField.e_dvd_e` `e_eq_one`
`n_dvd_f` 📖	mathematical	—	`IsNonarchimedeanLocalField.f`	—	`e_eq_one`
`n_eq_f` 📖	mathematical	—	`IsNonarchimedeanLocalField.f`	—	`e_eq_one`
`ofAlgEquiv` 📖	mathematical	—	`IsNonarchimedeanLocalField.IsUnramified`	—	`IsNonarchimedeanLocalField.e_congr` `e_eq_one`
`of_tower_bot` 📖	mathematical	—	`IsNonarchimedeanLocalField.IsUnramified`	—	`IsNonarchimedeanLocalField.e_dvd_e_bot` `e_eq_one`
`of_tower_top` 📖	mathematical	—	`IsNonarchimedeanLocalField.IsUnramified`	—	`IsNonarchimedeanLocalField.e_dvd_e_top` `e_eq_one`
`trans` 📖	mathematical	—	`IsNonarchimedeanLocalField.IsUnramified`	—	`IsNonarchimedeanLocalField.e_mul_e` `e_eq_one`

---

← Back to Index