English
The ring of integers of a number field K is the integral closure of Z in K.
Русский
Кольцо целых числа числа поля K является интегральным замыканием Z в K.
LaTeX
$$$$ \\mathcal{O}_K = \\text{integralClosure}_{\\mathbb{Z}}(K) $$$$
Lean4
/-- The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.
This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
-/
def RingOfIntegers : Type _ :=
integralClosure ℤ K
