Commit 2026-04-14 10:54 34dd2c69

View on Github →

feat(RingTheory): Order of vanishing in a discrete valuation ring (#29550) In this PR we develop some API for working with the order of vanishing in a discrete valuation ring.

Estimated changes

added theorem div_smul_div_comm
added theorem min_inv_inv_le
modified theorem Ring.ordFrac_eq_ord
added theorem Ring.ord_le_ord_mul
added theorem Ring.ord_le_ord_of_dvd
added theorem Ring.ord_le_smul
added theorem Ring.ord_lt_top
added theorem Ring.ord_mul'
added theorem Ring.ord_ne_top
added theorem Ring.ord_neg
added theorem Ring.ord_of_isUnit
added theorem Ring.ord_pow
added theorem Ring.ord_zero
added theorem Ring.ordFrac_add
added theorem Ring.ordFrac_le_smul
added theorem Ring.ordFrac_of_isUnit
added theorem Ring.ord_add
added theorem Ring.ord_eq_addVal
added theorem Ring.ord_le_iff