mathlib3 documentation


S-integers and S-units of fraction fields of Dedekind domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let K be the field of fractions of a Dedekind domain R, and let S be a set of prime ideals in the height one spectrum of R. An S-integer of K is defined to have v-adic valuation at most one for all primes ideals v away from S, whereas an S-unit of is defined to have v-adic valuation exactly one for all prime ideals v away from S.

This file defines the subalgebra of S-integers of K and the subgroup of S-units of , where K can be specialised to the case of a number field or a function field separately.

Main definitions #

Main statements #

References #

Tags #

S integer, S-integer, S unit, S-unit

S-integers #

The R-subalgebra of S-integers of K.


S-units #

noncomputable def set.unit {R : Type u} [comm_ring R] [is_domain R] [is_dedekind_domain R] (S : set (is_dedekind_domain.height_one_spectrum R)) (K : Type v) [field K] [algebra R K] [is_fraction_ring R K] :

The subgroup of S-units of .


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