Basic

📁 Source: ClassFieldTheory/IsNonarchimedeanLocalField/Basic.lean

Statistics

Metric	Count
Definitions `IsUnramified`, `compactOpenOK`, `e`, `equivResidueField`, `f`, `inhabitedIoo`, `instAlgebraResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `rankOneOfIoo`, `valuationOfIoo`	10
Theorems `isOpen_unramifiedLocus'`, `unramifiedLocus_eq_univ_iff'`, `ne_zero'`, `e_eq_one`, `toNNReal_exp`, `algebraMap_integers_apply_coe`, `algebraMap_mem_integer`, `associated_iff_of_irreducible`, `e_eq_one_of_n_eq_one`, `e_le_n`, `e_mul_f_eq_n`, `e_pos`, `e_spec`, `e_spec'`, `ext_extension`, `f_eq_one_of_n_eq_one`, `f_le_n`, `f_pos`, `f_spec`, `f_spec'`, `factors_map_maximalIdeal`, `instCompatibleNNRealValuationOfIoo`, `instContinuousSMul_classFieldTheory`, `instFaithfulSMulSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instFiniteDimensionalResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instFiniteDimensional_classFieldTheory`, `instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory`, `instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instIsLocalHomSubtypeMemSubringIntegerValueGroupWithZeroValuationRingHomAlgebraMap_classFieldTheory`, `instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1`, `instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1`, `instLiesOverSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory`, `instLocallyCompactSpacePadic_classFieldTheory`, `instPadic_classFieldTheory`, `instT2Space_classFieldTheory`, `isIntegralClosure`, `isIntegral_iff`, `isModuleTopology`, `isNonarchimedeanLocalField_of_finiteDimensional`, `isNonarchimedeanLocalField_of_valuativeExtension`, `isNonarchimedeanLocalField_of_valuativeExtension_of_isValuativeTopology`, `isUnramified_iff`, `isUnramified_iff_isUnramifiedAt`, `isUnramified_iff_map_maximalIdeal`, `isUnramified_iff_unramified`, `prime_ringChar`, `toFinset_factors_map_maximalIdeal`, `unique_isNonarchimedeanLocalField`, `valuationOfIoo_irreducible`, `valuation_ext`, `valuation_irreducible`, `valueGroupWithZeroIsoInt_irreducible`, `valuation_le_one_of_isIntegral`, `compatible`	56
Total	66
⚠️ With sorry `isOpen_unramifiedLocus'`, `unramifiedLocus_eq_univ_iff'`, `instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instPadic_classFieldTheory`	4

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_unramifiedLocus'` 📖 ⚠️	—	—	—	—	—
`unramifiedLocus_eq_univ_iff'` 📖 ⚠️	—	—	—	—	—

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ne_zero'` 📖	—	—	—	—	—

IsNonarchimedeanLocalField

Definitions

Name	Category	Theorems
`IsUnramified` 📖	CompData	14 math math: `IsUnramified.trans`, `isUnramified_iff_unramified`, `isUnramified_iff_isUnramifiedAt`, `le_maximalUnramified_iff`, `instIsUnramifiedSubtypeMemIntermediateFieldMaximalUnramified`, `instIsUnramifiedUnramifiedExtension`, `IsUnramified.of_tower_bot`, `IsUnramified.of_tower_top`, `isUnramified_iff`, `instIsUnramifiedSubtypeMemIntermediateFieldFieldRange`, `IsUnramified.comap`, `IsUnramified.ofAlgEquiv`, `InUnramified.intermediateField`, `isUnramified_iff_map_maximalIdeal`
`compactOpenOK` 📖	CompOp	—
`e` 📖	CompOp	15 math math: `e_congr`, `e_spec'`, `e_eq_one_of_n_eq_one`, `e_fieldRange`, `e_dvd_e_top`, `e_le_n`, `factors_map_maximalIdeal`, `isUnramified_iff`, `e_dvd_e`, `e_dvd_e_bot`, `e_spec`, `e_mul_e`, `e_mul_f_eq_n`, `IsUnramified.e_eq_one`, `e_pos`
`equivResidueField` 📖	CompOp	—
`f` 📖	CompOp	16 math math: `f_unramifiedExtension`, `IsUnramified.n_eq_f`, `f_spec'`, `f_spec`, `f_dvd_f_top`, `f_dvd_f`, `f_congr`, `f_mul_f`, `IsUnramified.n_dvd_f`, `nonempty_unramifiedExtension_alghom_iff_dvd_f`, `f_pos`, `f_eq_one_of_n_eq_one`, `f_fieldRange`, `f_dvd_f_bot`, `e_mul_f_eq_n`, `f_le_n`
`inhabitedIoo` 📖	CompOp	—
`instAlgebraResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	CompOp	5 math math: `instIsScalarTowerResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instFiniteDimensionalResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `f_spec`, `instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1`
`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	CompOp	14 math math: `e_spec'`, `instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_2`, `isUnramified_iff_unramified`, `isUnramified_iff_isUnramifiedAt`, `instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `toFinset_factors_map_maximalIdeal`, `factors_map_maximalIdeal`, `instLiesOverSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory`, `instFaithfulSMulSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `e_spec`, `instIsLocalHomSubtypeMemSubringIntegerValueGroupWithZeroValuationRingHomAlgebraMap_classFieldTheory`, `instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1`, `algebraMap_integers_apply_coe`, `isUnramified_iff_map_maximalIdeal`
`rankOneOfIoo` 📖	CompOp	—
`valuationOfIoo` 📖	CompOp	2 math math: `instCompatibleNNRealValuationOfIoo`, `valuationOfIoo_irreducible`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_integers_apply_coe` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	—
`algebraMap_mem_integer` 📖	—	—	—	—	`ValuativeExtension.algebraMap_le`
`associated_iff_of_irreducible` 📖	—	—	—	—	—
`e_eq_one_of_n_eq_one` 📖	mathematical	—	`e`	—	`e_le_n` `e_pos`
`e_le_n` 📖	mathematical	—	`e`	—	`e_mul_f_eq_n` `f_pos`
`e_mul_f_eq_n` 📖	mathematical	—	`e` `f`	—	`instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1` `instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `primesOverFinset.eq_1` `toFinset_factors_map_maximalIdeal`
`e_pos` 📖	mathematical	—	`e`	—	`instLiesOverSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory` `e_spec'`
`e_spec` 📖	mathematical	—	`e` `instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`instFaithfulSMulSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`e_spec'` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `e`	—	`e_spec`
`ext_extension` 📖	—	—	—	—	`ValuativeRel.ext_of_field` `isIntegral_iff` `isModuleTopology`
`f_eq_one_of_n_eq_one` 📖	mathematical	—	`f`	—	`f_le_n` `f_pos`
`f_le_n` 📖	mathematical	—	`f`	—	`e_mul_f_eq_n` `e_pos`
`f_pos` 📖	mathematical	—	`f`	—	`instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `instLiesOverSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory`
`f_spec` 📖	mathematical	—	`instAlgebraResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `f`	—	`instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`f_spec'` 📖	mathematical	—	`f`	—	`f_spec`
`factors_map_maximalIdeal` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `e`	—	`e_spec'` `IsDiscreteValuationRing.factors_maximalIdeal_pow`
`instCompatibleNNRealValuationOfIoo` 📖	mathematical	—	`valuationOfIoo`	—	`Valuation.compatible_map`
`instContinuousSMul_classFieldTheory` 📖	—	—	—	—	`isModuleTopology`
`instFaithfulSMulSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	—
`instFiniteDimensionalResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	mathematical	—	`instAlgebraResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`instIsLocalHomSubtypeMemSubringIntegerValueGroupWithZeroValuationRingHomAlgebraMap_classFieldTheory` `instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`instFiniteDimensional_classFieldTheory` 📖	—	—	—	—	`valuation_map_irreducible_lt_one` `Valued.toNormedField.compatible` `instCompatibleNNRealValuationOfIoo` `valuation_ext` `valuationOfIoo_irreducible` `Irreducible.ne_zero'`
`instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory` 📖	—	—	—	—	—
`instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖 ⚠️	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	—
`instIsLocalHomSubtypeMemSubringIntegerValueGroupWithZeroValuationRingHomAlgebraMap_classFieldTheory` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	—
`instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	—	—	—	—	—
`instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	—
`instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	mathematical	—	`instAlgebraResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	—
`instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1` 📖	mathematical	—	`instAlgebraResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	—
`instLiesOverSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`algebraMap_integers_apply_coe` `valuation_map_irreducible_lt_one`
`instLocallyCompactSpacePadic_classFieldTheory` 📖	—	—	—	—	—
`instPadic_classFieldTheory` 📖 ⚠️	—	—	—	—	`instLocallyCompactSpacePadic_classFieldTheory`
`instT2Space_classFieldTheory` 📖	—	—	—	—	—
`isIntegralClosure` 📖	—	—	—	—	`ValuativeExtension.valuation_le_one_of_isIntegral` `instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1` `instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`isIntegral_iff` 📖	—	—	—	—	`isIntegralClosure`
`isModuleTopology` 📖	—	—	—	—	`instContinuousSMul_classFieldTheory` `instFiniteDimensional_classFieldTheory` `instT2Space_classFieldTheory`
`isNonarchimedeanLocalField_of_finiteDimensional` 📖	—	—	—	—	`NormedField.compatible` `isNonarchimedeanLocalField_of_valuativeExtension`
`isNonarchimedeanLocalField_of_valuativeExtension` 📖	—	—	—	—	`isNonarchimedeanLocalField_of_valuativeExtension_of_isValuativeTopology`
`isNonarchimedeanLocalField_of_valuativeExtension_of_isValuativeTopology` 📖	—	—	—	—	`instContinuousSMul_classFieldTheory` `Irreducible.ne_zero'` `valuation_map_irreducible_lt_one`
`isUnramified_iff` 📖	mathematical	—	`IsUnramified` `e`	—	—
`isUnramified_iff_isUnramifiedAt` 📖	mathematical	—	`IsUnramified` `instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`isUnramified_iff_map_maximalIdeal` `instIsLocalHomSubtypeMemSubringIntegerValueGroupWithZeroValuationRingHomAlgebraMap_classFieldTheory` `Algebra.isUnramifiedAt_iff_map_eq'` `instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `instLiesOverSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory` `isLocalization_self` `instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1`
`isUnramified_iff_map_maximalIdeal` 📖	mathematical	—	`IsUnramified` `instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`isUnramified_iff` `e_spec'`
`isUnramified_iff_unramified` 📖	mathematical	—	`IsUnramified` `instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`Algebra.unramified_iff` `isUnramified_iff_isUnramifiedAt` `Algebra.unramifiedLocus_eq_univ_iff'` `Algebra.isOpen_unramifiedLocus'` `instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`prime_ringChar` 📖	—	—	—	—	—
`toFinset_factors_map_maximalIdeal` 📖	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`factors_map_maximalIdeal` `e_pos`
`unique_isNonarchimedeanLocalField` 📖	—	—	—	—	`isNonarchimedeanLocalField_of_finiteDimensional` `ext_extension`
`valuationOfIoo_irreducible` 📖	mathematical	—	`valuationOfIoo`	—	`valueGroupWithZeroIsoInt_irreducible` `WithZeroMulInt.toNNReal_exp`
`valuation_ext` 📖	—	—	—	—	`Valuation.ext_lt_one` `Valuation.Integers.associated_iff_eq`
`valuation_irreducible` 📖	—	—	—	—	`valueGroupWithZeroIsoInt_irreducible`
`valueGroupWithZeroIsoInt_irreducible` 📖	—	—	—	—	`WithZero.exp_neg_one_def` `le_valuation_irreducible_of_lt_one`

IsNonarchimedeanLocalField.IsUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`e_eq_one` 📖	mathematical	—	`IsNonarchimedeanLocalField.e`	—	—

IsNonarchimedeanLocalField.WithZeroMulInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toNNReal_exp` 📖	—	—	—	—	—

ValuativeExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`valuation_le_one_of_isIntegral` 📖	—	—	—	—	—

Valued.toNormedField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatible` 📖	—	—	—	—	`Valuation.compatible_map`

---

← Back to Index