Commit 2025-07-05 00:19 e8ef7e1d

View on Github →

feat(RingTheory/ValuativeRel): additional API to prepare for refactor (#26712) some helper lemmas that will be used in downstream refactor of Valued PRs

Estimated changes

Modified Mathlib/RingTheory/Valuation/ValuativeRel.lean

added theorem Valuation.Compatible.ofValuation

added theorem ValuativeRel.ValueGroupWithZero.lift_mul

added theorem ValuativeRel.ValueGroupWithZero.lift_one

added theorem ValuativeRel.ValueGroupWithZero.lift_valuation

added theorem ValuativeRel.ValueGroupWithZero.lift_zero

added theorem ValuativeRel.ValueGroupWithZero.mk_lt_mk