Commit 2026-10-19 12:30 bdece672

View on Github →

feat(RingTheory/Valuation/Discrete/IsDiscreteValuationSubring): equivalent discrete valuations (#43655) If v is equivalent to a discrete valuation, then v is discrete. In particular, if a ValuationSubring F A is a discrete valuation ring, then A.valuation is discrete.

Estimated changes

Modified Mathlib/RingTheory/Valuation/Basic.lean

added def Valuation.IsEquiv.orderMonoidIso

deleted theorem Valuation.IsEquiv.orderMonoidIso_eq_refl

modified theorem Valuation.IsEquiv.orderMonoidIso_spec

deleted theorem Valuation.IsEquiv.orderMonoidIso_spec₀

deleted theorem Valuation.IsEquiv.orderMonoidIso_symm

deleted theorem Valuation.IsEquiv.orderMonoidIso_trans

added theorem Valuation.IsEquiv.orderMonoidIso₀_coe

added theorem Valuation.IsEquiv.orderMonoidIso₀_eq_refl

added theorem Valuation.IsEquiv.orderMonoidIso₀_spec

added theorem Valuation.IsEquiv.orderMonoidIso₀_spec₀

added theorem Valuation.IsEquiv.orderMonoidIso₀_symm

added theorem Valuation.IsEquiv.orderMonoidIso₀_trans

deleted theorem Valuation.IsEquiv.valueGroup₀Fun_spec

deleted theorem Valuation.IsEquiv.valueGroup₀Fun_zero

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

added theorem Valuation.IsEquiv.isRankOneDiscrete_iff

added theorem Valuation.IsRankOneDiscrete.of_isEquiv

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

added theorem IsDiscreteValuationRing.maximalIdeal_valuation_isEquiv

Modified Mathlib/RingTheory/Valuation/Extension.lean

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

deleted theorem ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed

added theorem ValuativeRel.ValueGroupWithZero.orderMonoidIso₀_embed

Modified Mathlib/Topology/Algebra/Valued/WithVal.lean