Theorems · Definition · commutative algebra

AddValuation.onQuotVal

{R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] →
        (v : AddValuation R Γ₀) → {J : Ideal R} → J ≤ v.supp → R ⧸ J → Γ₀

If hJ : J ⊆ supp v then onQuotVal hJ is the induced function on R / J as a function. Note: it's just the function; the valuation is onQuot hJ.

Defined in

Mathlib.RingTheory.Valuation.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLinearOrderedAddCommMonoidWithTop