Theorems · Theorem · commutative algebra

Valuation.supp_quot

∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {J : Ideal R} (hJ : J ≤ v.supp), (v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp

The quotient valuation on R / J has support (supp v) / J if J ⊆ supp v.

Defined in

Mathlib.RingTheory.Valuation.Quotient

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingLinearOrderedCommMonoidWithZero