Commit 2025-11-20 13:23 8624f6f2

View on Github →

feat(RingTheory/Valuation): monotonicity of mul wrt SRel (#31783)

Estimated changes

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

added theorem ValuativeRel.ValueGroupWithZero.mk_pos

added theorem ValuativeRel.mul_rel_mul_iff_left

added theorem ValuativeRel.mul_rel_mul_iff_right

added theorem ValuativeRel.mul_srel_mul_iff_left

added theorem ValuativeRel.mul_srel_mul_iff_right

added theorem ValuativeRel.zero_srel_coe_posSubmonoid

modified theorem ValuativeRel.zero_srel_mul