Commit 2026-10-17 09:16 8c6a03c2

View on Github →

chore: split RingTheory/DedekindDomain/AdicValuation.lean into AdicValuation/Valuation.lean and AdicValuation/Completion.lean (#44666)

The file has grown quite large so split the HeightOneSpectrum.valuation material away from the completion material
Provides a more natural home for NumberTheory/RamificationInertia/Valuation.lean

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

Modified Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

Modified Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean

Modified Mathlib/NumberTheory/RamificationInertia/Valuation.lean

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_liesOver

deleted theorem IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOver

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_liesOver

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

deleted def IsDedekindDomain.HeightOneSpectrum.adicAbv

deleted def IsDedekindDomain.HeightOneSpectrum.adicAbvDef

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMap

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_of_mk'

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_add

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_mul

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_toCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupMulEquiv

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_zero

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_toCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderMonoidIso

deleted def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv

deleted def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.extension_apply_eq_valued

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.isUniformInducing_toCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_toCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_add

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_mul

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_ofCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_surjective

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_zero

deleted def IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformEquiv

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuationExtension_toCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation_ofCompletion

deleted def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquiv

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_coe

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_restrict

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroup_eq

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_apply

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_coe

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion_apply

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion_apply

deleted structure IsDedekindDomain.HeightOneSpectrum.adicCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one

deleted def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq

deleted def IsDedekindDomain.HeightOneSpectrum.adicValued

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply

deleted theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply

deleted theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion_toCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem

deleted theorem IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers

deleted theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion

deleted theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers

deleted theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap

deleted theorem IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuation

deleted theorem IsDedekindDomain.HeightOneSpectrum.exists_intValuation_mul_sub_lt

deleted theorem IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_of_integer

deleted theorem IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_or_mul_eq

deleted theorem IsDedekindDomain.HeightOneSpectrum.exists_valuation_sub_lt_of_integer

deleted theorem IsDedekindDomain.HeightOneSpectrum.exp_le_intValuation_iff_emultiplicity_le

deleted def IsDedekindDomain.HeightOneSpectrum.intAdicAbv

deleted def IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef

deleted theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff

deleted theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max'

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul'

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero'

deleted def IsDedekindDomain.HeightOneSpectrum.intValuation

deleted def IsDedekindDomain.HeightOneSpectrum.intValuationDef

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_apply

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_def

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_exp_neg_multiplicity

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_exp_iff_le_emultiplicity

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero'

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_singleton

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_uniformizer

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt

deleted theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv

deleted theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef

deleted theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbv

deleted theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbvDef

deleted theorem IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers

deleted theorem IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers

deleted def IsDedekindDomain.HeightOneSpectrum.valuation

deleted def IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_le_valuation

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_toSubring

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuationSubring_valuation_injective

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_def

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_one_iff_notMem

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer'

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_injective

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_le_one

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_surjective

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuation_uniformizer_ne_zero

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective

deleted theorem Rat.valuation_le_one_iff_den

Created Mathlib/RingTheory/DedekindDomain/AdicValuation/Completion.lean

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_add

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_mul

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_one

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupMulEquiv

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_zero

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderMonoidIso

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.extension_apply_eq_valued

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.isUniformInducing_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_add

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_mul

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_ofCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_one

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_surjective

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_zero

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformEquiv

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuationExtension_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation_ofCompletion

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquiv

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_coe

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_restrict

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroup_eq

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_apply

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_coe

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion_apply

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion_apply

added structure IsDedekindDomain.HeightOneSpectrum.adicCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one

added def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq

added def IsDedekindDomain.HeightOneSpectrum.adicValued

added theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply

added theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply

added theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem

added theorem IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap

added theorem IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'

added theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation

added theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective

Created Mathlib/RingTheory/DedekindDomain/AdicValuation/Ramification.lean

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_liesOver

added theorem IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOver

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_liesOver

Created Mathlib/RingTheory/DedekindDomain/AdicValuation/Valuation.lean

added def IsDedekindDomain.HeightOneSpectrum.adicAbv

added def IsDedekindDomain.HeightOneSpectrum.adicAbvDef

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMap

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_of_mk'

added theorem IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuation

added theorem IsDedekindDomain.HeightOneSpectrum.exists_intValuation_mul_sub_lt

added theorem IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_of_integer

added theorem IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_or_mul_eq

added theorem IsDedekindDomain.HeightOneSpectrum.exists_valuation_sub_lt_of_integer

added theorem IsDedekindDomain.HeightOneSpectrum.exp_le_intValuation_iff_emultiplicity_le

added def IsDedekindDomain.HeightOneSpectrum.intAdicAbv

added def IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef

added theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero'

added def IsDedekindDomain.HeightOneSpectrum.intValuation

added def IsDedekindDomain.HeightOneSpectrum.intValuationDef

added theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg

added theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos

added theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_apply

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_def

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_exp_neg_multiplicity

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_exp_iff_le_emultiplicity

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero'

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_singleton

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_uniformizer

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt

added theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv

added theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef

added theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbv

added theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbvDef

added theorem IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one

added def IsDedekindDomain.HeightOneSpectrum.valuation

added def IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime

added theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring

added theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_le_valuation

added theorem IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_toSubring

added theorem IsDedekindDomain.HeightOneSpectrum.valuationSubring_valuation_injective

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_def

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_one_iff_notMem

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer'

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_injective

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_surjective

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_uniformizer_ne_zero

added theorem Rat.valuation_le_one_iff_den

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/RingTheory/DedekindDomain/GaussLemma.lean

Modified Mathlib/RingTheory/DedekindDomain/SInteger.lean

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

Modified Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean