Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-26 18:06 8bc2354c

View on Github →

feat(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API (#14656) This PR defines the unique maximal ideal of a valuation subring as a subsemigroup of the field. We prove a few equivalent conditions for two valuations to be equivalent, and we use this to show two valuation subrings are equivalent iff they have the same maximal ideal.

Estimated changes

modified theorem add_valuation.map_inv
modified theorem add_valuation.ne_top_iff
modified theorem add_valuation.top_iff
modified theorem valuation.map_inv
modified theorem valuation.map_zpow
modified theorem valuation.ne_zero_iff
modified theorem valuation.zero_iff