Theorems · Definition · commutative algebra

NumberField.RingOfIntegers.withValEquiv

{Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {K : Type u_3} →
      [inst_1 : Field K] →
        (v : Valuation K Γ₀) →
          (R : Type u_4) →
            [inst_2 : CommRing R] →
              [inst_3 : Algebra R K] → [IsIntegralClosure R ℤ K] → NumberField.RingOfIntegers (WithVal v) ≃+* R

The ring equivalence between 𝓞 (WithVal v) and an integral closure of ℤ in K.

Defined in

Mathlib.Topology.Algebra.Valued.WithVal

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderedCommGroupWithZeroFieldCommRingAlgebraIsIntegralClosure