Mathlib Changelog
v4
Changelog
About
Github
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