Commit 2025-11-20 14:55 f924b1de

View on Github →

feat(Valuation): uniformizer of discrete valuation (#30259)

Estimated changes

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

added theorem ValuativeRel.IsNontrivial.exists_lt_one

added theorem ValuativeRel.le_uniformizer_iff

added def ValuativeRel.uniformizer

added theorem ValuativeRel.uniformizer_inv_le_iff

added theorem ValuativeRel.uniformizer_lt_one

added theorem ValuativeRel.uniformizer_ne_zero

added theorem ValuativeRel.uniformizer_pos