Commit 2026-06-03 06:54 c94dd590

View on Github →

feat(Valuation/ValuativeRel): generalize ValuativeRel to non-commutative rings (#36777) This is the second in a series of PRs, with the final goal of removing the class Valued from Mathlib. A Valued instance will be replaced by [ValuativeRel R] [UniformSpace R] [IsValuativeTopology R] [IsUniformAddGroup R] (v : Valuation R A) [v.Compatible]. This PR generalize ValuativeRel from CommRing to Semiring by adding a field vle_mul_comm {x y} : vle (x * y) (y * x). Without this field, the value group associated to the valuative relation may be non-abelian. The APIs of ValuativeRel.ofValuation and ValuativeRel.valuation are also generalized, showing this new definition is indeed equivalent to the valuations on non commutative rings. This is a prerequisite of #36769 .

Estimated changes

modified theorem ValuativeRel.mul_veq_mul
modified theorem ValuativeRel.not_vgt_of_veq
modified theorem ValuativeRel.not_vle
modified theorem ValuativeRel.not_vlt
modified theorem ValuativeRel.not_vlt_of_veq
modified theorem ValuativeRel.srel_iff
modified theorem ValuativeRel.veq_comm
modified theorem ValuativeRel.veq_def
modified theorem ValuativeRel.veq_rfl
modified theorem ValuativeRel.veq_trans
modified theorem ValuativeRel.vge_of_veq
modified theorem ValuativeRel.vle_mul_right
modified theorem ValuativeRel.vle_of_veq
modified theorem ValuativeRel.vle_rfl
modified theorem ValuativeRel.vle_trans'
modified theorem ValuativeRel.vlt.trans
modified theorem ValuativeRel.vlt.vle