Commit 2026-01-21 07:32 a8d00042

View on Github →

feat(RingTheory/Valuation/ValuativeRel): introduce =ᵥ relation (#33532) Of course, the characterizing property is that for any compatible valuation, x =ᵥ y is equivalent to v x = v y.

Estimated changes

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

added theorem Valuation.veq_iff_eq

added theorem ValuativeRel.mul_veq_mul

added theorem ValuativeRel.not_vgt_of_veq

added theorem ValuativeRel.not_vlt_of_veq

added def ValuativeRel.veq

added theorem ValuativeRel.veq_comm

added theorem ValuativeRel.veq_def

added theorem ValuativeRel.veq_refl

added theorem ValuativeRel.veq_rfl

added theorem ValuativeRel.veq_trans

added theorem ValuativeRel.veq_zero_iff

added theorem ValuativeRel.vge_of_veq

added theorem ValuativeRel.vle_of_veq

modified theorem ValuativeRel.vle_refl

modified theorem ValuativeRel.vle_rfl

added theorem ValuativeRel.zero_veq_iff