Theorems · Theorem · commutative algebra

ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier

∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : (PrimeSpectrum ↥A)ᵒᵈ),
  ↑↑(A.primeSpectrumOrderEquiv a) =
    {x | ∃ a_1 ∈ A, ∃ a_2, (∃ (x : a_2 ∈ A), ⟨a_2, ⋯⟩ ∉ (OrderDual.ofDual a).asIdeal) ∧ x = a_1 * a_2⁻¹}

Defined in

Mathlib.RingTheory.Valuation.ValuationSubring

Cited by

0 results in Mathlib

Foundations

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

Assumes

Field