Theorems · Theorem · commutative algebra

Ring.ord_add

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] (x y : R),
  min (Ring.ord R x) (Ring.ord R y) ≤ Ring.ord R (x + y)

For x y : R where R is a discrete valuation ring, we have that min (ord R x) (ord R y) ≤ ord R (x + y). It should be noted that the order we're using here is the order on ℕ∞, where ⊤ is greater than everything else. This is relevant since when we're working with ordFrac we work with ℤᵐ⁰, where the order instance has the 0 element less than everything else.

Defined in

Mathlib.RingTheory.OrderOfVanishing.Noetherian

Cited by

0 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainIsDiscreteValuationRing