Commit 2025-06-30 18:17 c5833050

View on Github →

chore(RingTheory/Valuation/Discrete/Basic): refactor the definition of discrete valuation to allow for more general targets (#23727) Co-authored by @mariainesdff The two ToDo mentioned in the docstring are WIP by María Inés de Frutos-Fernández and Filippo A. E. Nuccio.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GroupWithZero/Range.lean

added theorem MonoidHomWithZero.inv_mem_valueGroup

added theorem MonoidHomWithZero.mem_valueGroup

added theorem MonoidHomWithZero.mem_valueGroup_iff_of_comm

added theorem MonoidHomWithZero.mem_valueMonoid

added theorem MonoidHomWithZero.mem_valueMonoid_iff

added def MonoidHomWithZero.valueGroup

added theorem MonoidHomWithZero.valueGroup_def

added theorem MonoidHomWithZero.valueGroup_eq_range

added def MonoidHomWithZero.valueMonoid

added theorem MonoidHomWithZero.valueMonoid_eq_closure

added theorem MonoidHomWithZero.valueMonoid_eq_valueGroup'

added theorem MonoidHomWithZero.valueMonoid_eq_valueGroup

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

deleted theorem Valuation.IsDiscrete.surj

added theorem Valuation.IsRankOneDiscrete.exists_generator_lt_one

added theorem Valuation.IsRankOneDiscrete.generator_lt_one

added theorem Valuation.IsRankOneDiscrete.generator_mem_range

added theorem Valuation.IsRankOneDiscrete.generator_ne_one

added theorem Valuation.IsRankOneDiscrete.generator_ne_zero

added theorem Valuation.IsRankOneDiscrete.generator_zpowers_eq_range

added theorem Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup

deleted theorem Valuation.isDiscrete_iff_surjective