Theorems · Definition · number theory

Set.unit

{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] → Subgroup Kˣ

The subgroup of S-units of Kˣ.

Defined in

Mathlib.RingTheory.DedekindDomain.SInteger

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing