Commit 2025-07-01 23:25 2d1d0887

feat(ValuativeRel): Commutative rings endowed with a valuative relation (#26167) WIP -- comments welcome Commutative rings endowed with a valuative preorder (that is, a preorder arising from a valuation). This is equivalent to endowing a commutative ring with an equivalence class of a valuation, as opposed to an actual valuation. There is a "canonical" choice of a valuation associated to a valuative preorder obtain similarly to how one constructs a valuation from a valuation subring of a field.