Theorems · Theorem · commutative algebra

Ring.ordFrac_add

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (x y : K),
  x + y ≠ 0 → min ((Ring.ordFrac R) x) ((Ring.ordFrac R) y) ≤ (Ring.ordFrac R) (x + y)

For x y : R, if x + y ≠ 0 then min (ordFrac R x) (ordFrac R y) ≤ ordFrac R (x + y). The condition that x + y ≠ 0 is used to guarantee that all the elements we're taking ordFrac of are nonzero, meaning none of them will be 0 in ℤᵐ⁰. This allows us to use ord_add (which uses the ordering on ℕ∞), since these orders correspond on non ⊤ elements.

Defined in

Mathlib.RingTheory.OrderOfVanishing.Noetherian

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainIsDiscreteValuationRingFieldAlgebraIsFractionRing