Theorem ValuativeRel.mul_srel_mul_iff_right

Modification history

2025-11-20 13:23

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

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

Added ValuativeRel.mul_srel_mul_iff_right View on Github →