Documentation
Atlas
.
NumberTheoryI
.
code
.
Chapter1
.
NumberField
Search
return to top
source
Imports
Init
Mathlib.NumberTheory.NumberField.Basic
Imported by
number_field_and_ring_of_integers
source
theorem
number_field_and_ring_of_integers
(
K
:
Type
u_1)
[
Field
K
]
[
NumberField
K
]
:
FiniteDimensional
ℚ
K
∧
NumberField.RingOfIntegers
K
=
↥
(
integralClosure
ℤ
K
)