Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 23:36 b1a1ece3

View on Github →

feat(ring_theory/valuation/valuation_subring): The order structure on valuation subrings of a field (#13429) This PR shows that for a valuation subring R of a field K, the coarsenings of R are in (anti)ordered bijections with the prime ideals of R. As a corollary, the collection of such coarsenings is totally ordered.

Estimated changes

Modified src/algebra/hom/units.lean

Created src/ring_theory/localization/as_subring.lean

added theorem localization.map_is_unit_of_le

added def localization.map_to_fraction_ring

added theorem localization.map_to_fraction_ring_apply

added theorem localization.mem_range_map_to_fraction_ring_iff

added theorem localization.subalgebra.mem_range_map_to_fraction_ring_iff_of_field

added def localization.subalgebra.of_field

added def localization.subalgebra

Modified src/ring_theory/valuation/valuation_subring.lean

added theorem valuation_subring.add_mem

added def valuation_subring.ideal_of_le

added theorem valuation_subring.ideal_of_le_le_of_le

added theorem valuation_subring.ideal_of_le_of_prime

added def valuation_subring.inclusion

added theorem valuation_subring.le_of_prime

added def valuation_subring.map_of_le

added theorem valuation_subring.map_of_le_comp_valuation

added theorem valuation_subring.map_of_le_valuation_apply

added theorem valuation_subring.mem_of_subring

modified theorem valuation_subring.mem_of_valuation_le_one

added theorem valuation_subring.monotone_map_of_le

added theorem valuation_subring.mul_mem

added theorem valuation_subring.neg_mem

added def valuation_subring.of_le

added def valuation_subring.of_prime

added theorem valuation_subring.of_prime_ideal_of_le

added theorem valuation_subring.of_prime_le_of_le

added theorem valuation_subring.of_prime_valuation_eq_one_iff_mem_prime_compl

added def valuation_subring.of_subring

added theorem valuation_subring.one_mem

added def valuation_subring.prime_spectrum_equiv

added def valuation_subring.prime_spectrum_order_equiv

added def valuation_subring.subtype

modified def valuation_subring.valuation

added theorem valuation_subring.valuation_eq_one_iff

added theorem valuation_subring.valuation_lt_one_iff

added theorem valuation_subring.valuation_lt_one_or_eq_one

added theorem valuation_subring.valuation_unit

added def valuation_subring.value_group

added theorem valuation_subring.zero_mem