Commit 2025-11-17 13:13 cf9ef827

View on Github →

feat(RingTheory): API for valuative rel (#30423)

Estimated changes

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

deleted theorem Valuation.Compatible.srel_iff_lt

modified theorem Valuation.apply_posSubmonoid_ne_zero

modified theorem Valuation.apply_posSubmonoid_pos

added theorem Valuation.one_rel_iff

added theorem Valuation.one_srel_iff

added theorem Valuation.rel_iff_le

added theorem Valuation.rel_one_iff

added theorem Valuation.srel_iff_lt

added theorem Valuation.srel_one_iff

added theorem ValuativeExtension.mapValueGroupWithZero_strictMono

added theorem ValuativeRel.IsRankLeOne.of_valuativeExtension

added theorem ValuativeRel.SRel.rel

added theorem ValuativeRel.SRel.trans

added def ValuativeRel.SRel

added theorem ValuativeRel.div_rel_iff

added theorem ValuativeRel.div_rel_one_iff

added theorem ValuativeRel.inv_rel_one

added theorem ValuativeRel.inv_srel_one

added theorem ValuativeRel.mul_rel_mul

added theorem ValuativeRel.mul_srel_mul

added theorem ValuativeRel.mul_srel_mul_of_rel_of_srel

added theorem ValuativeRel.mul_srel_mul_of_srel_of_rel

added theorem ValuativeRel.one_rel_div_iff

added theorem ValuativeRel.one_rel_inv

added theorem ValuativeRel.one_srel_inv

added theorem ValuativeRel.pow_rel_pow

added theorem ValuativeRel.pow_rel_pow_of_one_rel

added theorem ValuativeRel.pow_rel_pow_of_rel_one

added theorem ValuativeRel.pow_srel_pow

added theorem ValuativeRel.rel_div_iff

deleted theorem ValuativeRel.rel_mul

modified theorem ValuativeRel.rel_mul_left

added theorem ValuativeRel.rel_mul_left_iff

added theorem ValuativeRel.rel_mul_right_iff

added theorem ValuativeRel.rel_zero_iff

deleted def ValuativeRel.srel

added theorem ValuativeRel.srel_mul_left_iff

added theorem ValuativeRel.srel_mul_right_iff

added theorem ValuativeRel.srel_of_rel_of_srel

added theorem ValuativeRel.srel_of_srel_of_rel

added theorem ValuativeRel.zero_srel_iff

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