Theorems · Definition · number theory

Set.integer

{R : Type u} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      Set (IsDedekindDomain.HeightOneSpectrum R) →
        (K : Type v) → [inst_2 : Field K] → [inst_3 : Algebra R K] → [IsFractionRing R K] → Subalgebra R K

The R-subalgebra of S-integers of K.

Defined in

Mathlib.RingTheory.DedekindDomain.SInteger

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing