Theorems · Definition · number theory

Set.unitEquivUnitsInteger

{R : Type u} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (S : Set (IsDedekindDomain.HeightOneSpectrum R)) →
        (K : Type v) →
          [inst_2 : Field K] → [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → ↥(S.unit K) ≃* (↥(S.integer K))ˣ

The group of S-units is the group of units of the ring of S-integers.

Defined in

Mathlib.RingTheory.DedekindDomain.SInteger

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing