Commit 2025-07-11 14:29 75f8149d

View on Github →

feat(RingTheory/Valuation/Discrete/Basic): add uniformizer API (#26591) We define uniformizers for discrete valuations.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Range.lean

Modified Mathlib/Algebra/Order/Group/Cyclic.lean

added theorem LinearOrderedCommGroup.Subgroup.genLTOne_mem

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

modified theorem Valuation.IsRankOneDiscrete.exists_generator_lt_one

modified theorem Valuation.IsRankOneDiscrete.generator_lt_one

added theorem Valuation.IsRankOneDiscrete.generator_mem_valueGroup

modified theorem Valuation.IsRankOneDiscrete.generator_ne_one

modified theorem Valuation.IsRankOneDiscrete.generator_ne_zero

modified theorem Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup

added theorem Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator

added theorem Valuation.IsUniformizer.iff

added theorem Valuation.IsUniformizer.is_generator

added theorem Valuation.IsUniformizer.ne_zero

added theorem Valuation.IsUniformizer.not_isUnit

added theorem Valuation.IsUniformizer.of_associated

added theorem Valuation.IsUniformizer.val

added theorem Valuation.IsUniformizer.val_lt_one

added theorem Valuation.IsUniformizer.val_ne_zero

added theorem Valuation.IsUniformizer.val_pos

added theorem Valuation.IsUniformizer.zpowers_eq_valueGroup

added def Valuation.IsUniformizer

added theorem Valuation.Uniformizer.is_generator

added def Valuation.Uniformizer.mk'

added theorem Valuation.Uniformizer.ne_zero

added structure Valuation.Uniformizer

added theorem Valuation.associated_of_isUniformizer

added theorem Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial

added theorem Valuation.exists_pow_Uniformizer

added theorem Valuation.isUniformizer_of_maximalIdeal_eq_span

added theorem Valuation.pow_Uniformizer_is_pow_generator

added theorem Valuation.valuationSubring_not_isField

Modified docs/references.bib