Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-29 09:36 4bf4d9df

View on Github →

feat(ring_theory/dedekind_domain/adic_valuation): add adic valuation on a Dedekind domain (#12712) Given a Dedekind domain R of Krull dimension 1 and a maximal ideal v of R, we define the v-adic valuation on R and prove some of its properties, including the existence of uniformizers.

Estimated changes

Modified src/algebra/order/monoid.lean

added theorem with_zero.le_max_iff

added theorem with_zero.min_le_iff

Created src/ring_theory/dedekind_domain/adic_valuation.lean

added theorem is_dedekind_domain.height_one_spectrum.int_valuation.le_max_iff_min_le

added theorem is_dedekind_domain.height_one_spectrum.int_valuation.map_add_le_max'

added theorem is_dedekind_domain.height_one_spectrum.int_valuation.map_mul'

added theorem is_dedekind_domain.height_one_spectrum.int_valuation.map_one'

added theorem is_dedekind_domain.height_one_spectrum.int_valuation.map_zero'

added def is_dedekind_domain.height_one_spectrum.int_valuation

added def is_dedekind_domain.height_one_spectrum.int_valuation_def

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_def_if_neg

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_def_if_pos

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_exists_uniformizer

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_le_one

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_le_pow_iff_dvd

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_lt_one_iff_dvd

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_ne_zero'

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_ne_zero

added theorem is_dedekind_domain.height_one_spectrum.int_valuation_zero_le

Modified src/ring_theory/dedekind_domain/ideal.lean

added theorem associates.le_singleton_iff

deleted theorem is_dedekind_domain.height_one_spectrum.associates.irreducible

added theorem is_dedekind_domain.height_one_spectrum.associates_irreducible

Modified src/ring_theory/ideal/operations.lean

added theorem associates.mk_ne_zero'