theorem number_field_and_ring_of_integers (K : Type u_1) [Field K] [NumberField K] : FiniteDimensional ℚ K ∧ NumberField.RingOfIntegers K = ↥(integralClosure ℤ K)