Commit 2023-06-22 15:02 a53975a7

View on Github →

feat: port RingTheory.DedekindDomain.AdicValuation (#5372)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Monoid/WithZero/Defs.lean

Modified Mathlib/NumberTheory/FunctionField.lean

Created Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

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.adicCompletion

added def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

added def IsDedekindDomain.HeightOneSpectrum.adicValued

added theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply

added theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adic_completion'

added theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers

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.int_valuation_exists_uniformizer

added theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd

added theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_lt_one_iff_dvd

added theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero'

added theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero

added theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_zero_le

added theorem IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers

added def IsDedekindDomain.HeightOneSpectrum.valuation

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_def

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_uniformizer_ne_zero

added theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

modified theorem IsDedekindDomain.HeightOneSpectrum.prime

Modified Mathlib/Topology/Algebra/UniformField.lean

Modified Mathlib/Topology/Algebra/UniformMulAction.lean