Commit 2025-10-06 16:30 207daae0

View on Github →

feat(RingTheory/Valuation/ValuativeRel): strict valuative relation (#30262) extracted out of #27163 a way of discussing unbundled posSubmonoid

Estimated changes

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

added theorem Valuation.Compatible.srel_iff_lt

added theorem ValuativeExtension.srel_iff_srel

added theorem ValuativeRel.not_srel_iff

modified theorem ValuativeRel.posSubmonoid_def

added def ValuativeRel.srel

added theorem ValuativeRel.srel_iff

added theorem ValuativeRel.zero_srel_mul

added theorem ValuativeRel.zero_srel_one