Unramified

📁 Source: ClassFieldTheory/IsNonarchimedeanLocalField/Unramified.lean

Statistics

Metric	Count
Definitions `UnramifiedExtension`, `instAlgebraUnramifiedExtension`, `instFieldUnramifiedExtension`, `instFiniteDimensionalUnramifiedExtension`, `instTopologicalSpaceUnramifiedExtension`, `instValuativeRelUnramifiedExtension`, `maximalUnramified`	7
Theorems `intermediateFieldTop_eq_adjoin_primitive_root`, `isSplittingField`, `splits`, `top_eq_adjoin_primitive_root`, `top_eq_adjoin_roots`, `card_pow_sub_one_in_nat_ne_zero`, `card_pow_sub_one_ne_zero`, `card_pow_sub_one_ne_zero'`, `card_residue_pow_sub_one_in_field_ne_zero`, `card_residue_pow_sub_one_in_integers_ne_zero`, `f_unramifiedExtension`, `finrank_unramifiedExtension`, `finrank_unramifiedExtension_zero`, `instHasEnoughRootsOfUnityHSubNatCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat_classFieldTheory`, `instHasEnoughRootsOfUnityUnramifiedExtensionHSubNatHPowCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat`, `instIsGaloisOfIsUnramified`, `instIsGaloisUnramifiedExtension`, `instIsUnramifiedSubtypeMemIntermediateFieldMaximalUnramified`, `instIsUnramifiedUnramifiedExtension`, `instSubsingletonIntermediateFieldUnramifiedExtensionOfNatNat`, `instSubsingletonSubalgebraUnramifiedExtensionOfNatNat`, `instUnramifiedExtension`, `instValuativeExtensionUnramifiedExtension`, `le_maximalUnramified_iff`, `nonempty_unramifiedExtension_algEquiv_of_isUnramified`, `nonempty_unramifiedExtension_alghom_iff_dvd_f`, `nonempty_unramifiedExtension_alghom_of_dvd_f`	27
Total	34

IsNonarchimedeanLocalField

Definitions

Name	Category	Theorems
`UnramifiedExtension` 📖	CompOp	18 math math: `f_unramifiedExtension`, `finrank_unramifiedExtension_zero`, `UnramifiedExtension.splits`, `instSubsingletonIntermediateFieldUnramifiedExtensionOfNatNat`, `instHasEnoughRootsOfUnityUnramifiedExtensionHSubNatHPowCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat`, `UnramifiedExtension.top_eq_adjoin_roots`, `nonempty_unramifiedExtension_algEquiv_of_isUnramified`, `instSubsingletonSubalgebraUnramifiedExtensionOfNatNat`, `instIsUnramifiedUnramifiedExtension`, `UnramifiedExtension.intermediateFieldTop_eq_adjoin_primitive_root`, `UnramifiedExtension.top_eq_adjoin_primitive_root`, `nonempty_unramifiedExtension_alghom_of_dvd_f`, `nonempty_unramifiedExtension_alghom_iff_dvd_f`, `finrank_unramifiedExtension`, `instIsGaloisUnramifiedExtension`, `UnramifiedExtension.isSplittingField`, `instValuativeExtensionUnramifiedExtension`, `instUnramifiedExtension`
`instAlgebraUnramifiedExtension` 📖	CompOp	15 math math: `f_unramifiedExtension`, `finrank_unramifiedExtension_zero`, `instSubsingletonIntermediateFieldUnramifiedExtensionOfNatNat`, `UnramifiedExtension.top_eq_adjoin_roots`, `nonempty_unramifiedExtension_algEquiv_of_isUnramified`, `instSubsingletonSubalgebraUnramifiedExtensionOfNatNat`, `instIsUnramifiedUnramifiedExtension`, `UnramifiedExtension.intermediateFieldTop_eq_adjoin_primitive_root`, `UnramifiedExtension.top_eq_adjoin_primitive_root`, `nonempty_unramifiedExtension_alghom_of_dvd_f`, `nonempty_unramifiedExtension_alghom_iff_dvd_f`, `finrank_unramifiedExtension`, `instIsGaloisUnramifiedExtension`, `UnramifiedExtension.isSplittingField`, `instValuativeExtensionUnramifiedExtension`
`instFieldUnramifiedExtension` 📖	CompOp	18 math math: `f_unramifiedExtension`, `finrank_unramifiedExtension_zero`, `UnramifiedExtension.splits`, `instSubsingletonIntermediateFieldUnramifiedExtensionOfNatNat`, `instHasEnoughRootsOfUnityUnramifiedExtensionHSubNatHPowCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat`, `UnramifiedExtension.top_eq_adjoin_roots`, `nonempty_unramifiedExtension_algEquiv_of_isUnramified`, `instSubsingletonSubalgebraUnramifiedExtensionOfNatNat`, `instIsUnramifiedUnramifiedExtension`, `UnramifiedExtension.intermediateFieldTop_eq_adjoin_primitive_root`, `UnramifiedExtension.top_eq_adjoin_primitive_root`, `nonempty_unramifiedExtension_alghom_of_dvd_f`, `nonempty_unramifiedExtension_alghom_iff_dvd_f`, `finrank_unramifiedExtension`, `instIsGaloisUnramifiedExtension`, `UnramifiedExtension.isSplittingField`, `instValuativeExtensionUnramifiedExtension`, `instUnramifiedExtension`
`instFiniteDimensionalUnramifiedExtension` 📖	CompOp	—
`instTopologicalSpaceUnramifiedExtension` 📖	CompOp	3 math math: `f_unramifiedExtension`, `instIsUnramifiedUnramifiedExtension`, `instUnramifiedExtension`
`instValuativeRelUnramifiedExtension` 📖	CompOp	4 math math: `f_unramifiedExtension`, `instIsUnramifiedUnramifiedExtension`, `instValuativeExtensionUnramifiedExtension`, `instUnramifiedExtension`
`maximalUnramified` 📖	CompOp	2 math math: `le_maximalUnramified_iff`, `instIsUnramifiedSubtypeMemIntermediateFieldMaximalUnramified`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_pow_sub_one_in_nat_ne_zero` 📖	—	—	—	—	`card_pow_sub_one_ne_zero'`
`card_pow_sub_one_ne_zero` 📖	—	—	—	—	`card_pow_sub_one_ne_zero'`
`card_pow_sub_one_ne_zero'` 📖	—	—	—	—	—
`card_residue_pow_sub_one_in_field_ne_zero` 📖	—	—	—	—	`card_residue_pow_sub_one_in_integers_ne_zero`
`card_residue_pow_sub_one_in_integers_ne_zero` 📖	—	—	—	—	`card_pow_sub_one_ne_zero`
`f_unramifiedExtension` 📖	mathematical	—	`f` `UnramifiedExtension` `instFieldUnramifiedExtension` `instValuativeRelUnramifiedExtension` `instTopologicalSpaceUnramifiedExtension` `instUnramifiedExtension` `instAlgebraUnramifiedExtension` `instValuativeExtensionUnramifiedExtension`	—	`instUnramifiedExtension` `instValuativeExtensionUnramifiedExtension` `finrank_unramifiedExtension` `f_le_n` `instLiesOverSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory`
`finrank_unramifiedExtension` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instAlgebraUnramifiedExtension`	—	`instUnramifiedExtension` `instValuativeExtensionUnramifiedExtension`
`finrank_unramifiedExtension_zero` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instAlgebraUnramifiedExtension`	—	`UnramifiedExtension.isSplittingField`
`instHasEnoughRootsOfUnityHSubNatCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat_classFieldTheory` 📖	—	—	—	—	`FiniteField.instHasEnoughRootsOfUnityHSubNatCardOfNat_classFieldTheory` `teichmuller_injective`
`instHasEnoughRootsOfUnityUnramifiedExtensionHSubNatHPowCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension`	—	`HasEnoughRootsOfUnity.of_splits` `UnramifiedExtension.splits` `card_residue_pow_sub_one_in_field_ne_zero` `instUnramifiedExtension` `instValuativeExtensionUnramifiedExtension`
`instIsGaloisOfIsUnramified` 📖	—	—	—	—	`nonempty_unramifiedExtension_algEquiv_of_isUnramified` `instIsGaloisUnramifiedExtension`
`instIsGaloisUnramifiedExtension` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instAlgebraUnramifiedExtension`	—	`finrank_unramifiedExtension_zero` `UnramifiedExtension.isSplittingField` `card_residue_pow_sub_one_in_field_ne_zero` `ValuativeExtension.inst_classFieldTheory`
`instIsUnramifiedSubtypeMemIntermediateFieldMaximalUnramified` 📖	mathematical	—	`IsUnramified` `maximalUnramified` `ValuativeRel.instSubtypeMem_classFieldTheory` `instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1`	—	`instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1` `instIsUnramifiedSubtypeMemIntermediateFieldFieldRange` `instUnramifiedExtension` `instValuativeExtensionUnramifiedExtension` `instIsUnramifiedUnramifiedExtension`
`instIsUnramifiedUnramifiedExtension` 📖	mathematical	—	`IsUnramified` `UnramifiedExtension` `instFieldUnramifiedExtension` `instValuativeRelUnramifiedExtension` `instTopologicalSpaceUnramifiedExtension` `instUnramifiedExtension` `instAlgebraUnramifiedExtension` `instValuativeExtensionUnramifiedExtension`	—	`instUnramifiedExtension` `instValuativeExtensionUnramifiedExtension` `e_eq_one_of_n_eq_one` `finrank_unramifiedExtension_zero` `f_pos` `e_mul_f_eq_n` `finrank_unramifiedExtension` `f_unramifiedExtension`
`instSubsingletonIntermediateFieldUnramifiedExtensionOfNatNat` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instAlgebraUnramifiedExtension`	—	`instSubsingletonSubalgebraUnramifiedExtensionOfNatNat`
`instSubsingletonSubalgebraUnramifiedExtensionOfNatNat` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instAlgebraUnramifiedExtension`	—	`finrank_unramifiedExtension_zero`
`instUnramifiedExtension` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instValuativeRelUnramifiedExtension` `instTopologicalSpaceUnramifiedExtension`	—	`isNonarchimedeanLocalField_of_finiteDimensional`
`instValuativeExtensionUnramifiedExtension` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instValuativeRelUnramifiedExtension` `instAlgebraUnramifiedExtension`	—	`isNonarchimedeanLocalField_of_finiteDimensional`
`le_maximalUnramified_iff` 📖	mathematical	—	`maximalUnramified` `IsUnramified` `ValuativeRel.instSubtypeMem_classFieldTheory` `instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1`	—	`instSubtypeMemIntermediateField_classFieldTheory` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory_1` `IsUnramified.comap` `instIsUnramifiedSubtypeMemIntermediateFieldMaximalUnramified` `nonempty_unramifiedExtension_algEquiv_of_isUnramified` `IsUnramified.n_dvd_f` `f_dvd_f_top` `ValuativeRel.instValuativeExtensionSubtypeMem_classFieldTheory` `nonempty_unramifiedExtension_alghom_of_dvd_f` `instUnramifiedExtension` `instValuativeExtensionUnramifiedExtension` `f_unramifiedExtension` `f_pos` `instIsGaloisOfIsUnramified`
`nonempty_unramifiedExtension_algEquiv_of_isUnramified` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instAlgebraUnramifiedExtension`	—	`nonempty_unramifiedExtension_alghom_of_dvd_f` `IsUnramified.n_dvd_f` `instFiniteDimensional_classFieldTheory` `finrank_unramifiedExtension`
`nonempty_unramifiedExtension_alghom_iff_dvd_f` 📖	mathematical	—	`UnramifiedExtension` `instFieldUnramifiedExtension` `instAlgebraUnramifiedExtension` `f`	—	`instUnramifiedExtension` `instValuativeExtensionUnramifiedExtension` `f_dvd_f` `f_unramifiedExtension` `nonempty_unramifiedExtension_alghom_of_dvd_f`
`nonempty_unramifiedExtension_alghom_of_dvd_f` 📖	mathematical	`f`	`UnramifiedExtension` `instFieldUnramifiedExtension` `instAlgebraUnramifiedExtension`	—	`f_pos` `instHasEnoughRootsOfUnityUnramifiedExtensionHSubNatHPowCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat` `card_pow_sub_one_in_nat_ne_zero` `f_spec'` `instHasEnoughRootsOfUnityHSubNatCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat_classFieldTheory` `UnramifiedExtension.intermediateFieldTop_eq_adjoin_primitive_root`

IsNonarchimedeanLocalField.UnramifiedExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intermediateFieldTop_eq_adjoin_primitive_root` 📖	mathematical	`IsNonarchimedeanLocalField.UnramifiedExtension` `IsNonarchimedeanLocalField.instFieldUnramifiedExtension`	`IsNonarchimedeanLocalField.UnramifiedExtension` `IsNonarchimedeanLocalField.instFieldUnramifiedExtension` `IsNonarchimedeanLocalField.instAlgebraUnramifiedExtension`	—	`top_eq_adjoin_primitive_root`
`isSplittingField` 📖	mathematical	—	`IsNonarchimedeanLocalField.UnramifiedExtension` `IsNonarchimedeanLocalField.instFieldUnramifiedExtension` `IsNonarchimedeanLocalField.instAlgebraUnramifiedExtension`	—	—
`splits` 📖	mathematical	—	`IsNonarchimedeanLocalField.UnramifiedExtension` `IsNonarchimedeanLocalField.instFieldUnramifiedExtension`	—	`isSplittingField`
`top_eq_adjoin_primitive_root` 📖	mathematical	`IsNonarchimedeanLocalField.UnramifiedExtension` `IsNonarchimedeanLocalField.instFieldUnramifiedExtension`	`IsNonarchimedeanLocalField.UnramifiedExtension` `IsNonarchimedeanLocalField.instFieldUnramifiedExtension` `IsNonarchimedeanLocalField.instAlgebraUnramifiedExtension`	—	`IsNonarchimedeanLocalField.instSubsingletonSubalgebraUnramifiedExtensionOfNatNat` `IsNonarchimedeanLocalField.card_pow_sub_one_in_nat_ne_zero` `top_eq_adjoin_roots` `HasEnoughRootsOfUnity.exists_pow` `IsNonarchimedeanLocalField.instHasEnoughRootsOfUnityUnramifiedExtensionHSubNatHPowCardResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationOfNat`
`top_eq_adjoin_roots` 📖	mathematical	—	`IsNonarchimedeanLocalField.UnramifiedExtension` `IsNonarchimedeanLocalField.instFieldUnramifiedExtension` `IsNonarchimedeanLocalField.instAlgebraUnramifiedExtension`	—	`isSplittingField`

---

← Back to Index