Theorem ValuativeRel.mul_rel_mul_iff_left

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_rel_mul_iff_left View on Github →