AdicValuation

📁 Source: FLT/DedekindDomain/AdicValuation.lean

Statistics

Metric	Count
Definitions ResidueFieldEquivCompletionResidueField, ResidueFieldToCompletionResidueField, completionIdeal	3
Theorems eq_mul_nonZeroDivisor_inv_adicCompletionIntegers, eq_mul_pi_adicCompletionIntegers, eq_pow_uniformizer_mul_unit, exists_uniformizer, instDimensionLEOneSubtypeMemValuationSubringAdicCompletionIntegers_fLT, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeInt_fLT, instIsDiscreteValuationRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT, instIsPrincipalIdealRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT, maximalIdeal_eq_span_uniformizer, mem_completionIdeal_pow, uniformizer_ne_zero, uniformizer_not_isUnit, algebraMap_completionIntegers, closureAlgebraMapIntegers_eq_integers, closureAlgebraMapIntegers_eq_prodIntegers, completionIdeal_ne_bot, denseRange_of_integerAlgebraMap, denseRange_of_prodAlgebraMap, emultiplicity_eq_of_valuation_eq_ofAdd, exists_adicValued_mul_sub_le, exists_adicValued_sub_lt_of_adicCompletionInteger, exists_adicValued_sub_lt_of_adicValued_le_one, exists_forall_adicValued_sub_lt, exists_ofAdd_natCast_lt, exists_ofAdd_natCast_of_le_one, inertiaDeg_asIdeal_completionIdeal, instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal, mem_completionIdeal_iff, mem_completionIdeal_iff', ne_zero_of_some_le_intValuation	30
Total	33

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
ResidueFieldEquivCompletionResidueField 📖	CompOp	—
ResidueFieldToCompletionResidueField 📖	CompOp	—
completionIdeal 📖	CompOp	7 math math: instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal, adicCompletion.ramificationIdx_eq_ramificationIdx, adicCompletion.mem_completionIdeal_pow, mem_completionIdeal_iff, adicCompletion.inertiaDeg_eq_inertiaDeg, inertiaDeg_asIdeal_completionIdeal, mem_completionIdeal_iff'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_completionIntegers 📖	—	—	—	—	—
closureAlgebraMapIntegers_eq_integers 📖	—	—	—	—	exists_adicValued_sub_lt_of_adicValued_le_one
closureAlgebraMapIntegers_eq_prodIntegers 📖	—	—	—	—	exists_forall_adicValued_sub_lt
completionIdeal_ne_bot 📖	—	—	—	—	adicCompletion.instIsDiscreteValuationRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT
denseRange_of_integerAlgebraMap 📖	—	—	—	—	closureAlgebraMapIntegers_eq_integers
denseRange_of_prodAlgebraMap 📖	—	—	—	—	closureAlgebraMapIntegers_eq_prodIntegers adicCompletion.eq_mul_pi_adicCompletionIntegers
emultiplicity_eq_of_valuation_eq_ofAdd 📖	—	—	—	—	ne_zero_of_some_le_intValuation
exists_adicValued_mul_sub_le 📖	—	—	—	—	exists_ofAdd_natCast_of_le_one ne_zero_of_some_le_intValuation emultiplicity_eq_of_valuation_eq_ofAdd intValuation_eq_coe_neg_multiplicity
exists_adicValued_sub_lt_of_adicCompletionInteger 📖	—	—	—	—	closureAlgebraMapIntegers_eq_integers
exists_adicValued_sub_lt_of_adicValued_le_one 📖	—	—	—	—	exists_adicValued_mul_sub_le
exists_forall_adicValued_sub_lt 📖	—	—	—	—	exists_ofAdd_natCast_lt exists_adicValued_sub_lt_of_adicCompletionInteger
exists_ofAdd_natCast_lt 📖	—	—	—	—	—
exists_ofAdd_natCast_of_le_one 📖	—	—	—	—	—
inertiaDeg_asIdeal_completionIdeal 📖	mathematical	—	completionIdeal	—	instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal
instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal 📖	mathematical	—	completionIdeal	—	—
mem_completionIdeal_iff 📖	mathematical	—	completionIdeal	—	—
mem_completionIdeal_iff' 📖	mathematical	—	completionIdeal	—	adicCompletion.mem_completionIdeal_pow
ne_zero_of_some_le_intValuation 📖	—	—	—	—	—

IsDedekindDomain.HeightOneSpectrum.adicCompletion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_mul_nonZeroDivisor_inv_adicCompletionIntegers 📖	—	—	—	—	—
eq_mul_pi_adicCompletionIntegers 📖	—	—	—	—	eq_mul_nonZeroDivisor_inv_adicCompletionIntegers
eq_pow_uniformizer_mul_unit 📖	—	—	—	—	ValuationSubring.isUnit_of_valued_eq_one uniformizer_ne_zero
exists_uniformizer 📖	—	—	—	—	—
instDimensionLEOneSubtypeMemValuationSubringAdicCompletionIntegers_fLT 📖	—	—	—	—	exists_uniformizer eq_pow_uniformizer_mul_unit IsLocalRing.maximalIdeal_le maximalIdeal_eq_span_uniformizer
instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeInt_fLT 📖	—	—	—	—	instIsDiscreteValuationRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT
instIsDiscreteValuationRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT 📖	—	—	—	—	instIsPrincipalIdealRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT exists_uniformizer maximalIdeal_eq_span_uniformizer uniformizer_ne_zero
instIsPrincipalIdealRingSubtypeMemValuationSubringAdicCompletionIntegers_fLT 📖	—	—	—	—	exists_uniformizer instDimensionLEOneSubtypeMemValuationSubringAdicCompletionIntegers_fLT maximalIdeal_eq_span_uniformizer
maximalIdeal_eq_span_uniformizer 📖	—	—	—	—	uniformizer_not_isUnit eq_pow_uniformizer_mul_unit
mem_completionIdeal_pow 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.completionIdeal	—	exists_uniformizer maximalIdeal_eq_span_uniformizer uniformizer_ne_zero
uniformizer_ne_zero 📖	—	—	—	—	—
uniformizer_not_isUnit 📖	—	—	—	—	ValuationSubring.isUnit_iff_valued_eq_one

---

← Back to Index