theorem MaximalOrder.ringOfIntegers_isOrder (K : Type u_1) [Field K] [NumberField K] : Module.Free ℤ (NumberField.RingOfIntegers K) ∧ Module.finrank ℤ (NumberField.RingOfIntegers K) = Module.finrank ℚ K

The ring of integers 𝓞 K of a number field K is a ℤ-order: it is a free ℤ-module whose rank equals the ℚ-dimension of K. This is the order property needed for Theorem 12.26 (the ring of integers is the unique maximal order).

theorem MaximalOrder.ringOfIntegers_isMaximalOrder (K : Type u_1) [Field K] [NumberField K] (O : Subalgebra ℤ K) [Module.Finite ℤ ↥O] : O ≤ integralClosure ℤ K

Any ℤ-order O in a number field K is contained in the integral closure of ℤ in K (i.e. in 𝓞 K). This is the "containment half" of Theorem 12.26 expressing that the ring of integers is the unique maximal order.

theorem MaximalOrder.ringOfIntegers_unique_maximalOrder (K : Type u_1) [Field K] [NumberField K] (O : Subalgebra ℤ K) [Module.Finite ℤ ↥O] (hmax : ∀ (O' : Subalgebra ℤ K) [Module.Finite ℤ ↥O'], O ≤ O' → O' ≤ O) : O = integralClosure ℤ K

Theorem 12.26: the ring of integers 𝓞 K of a number field K is the unique maximal ℤ-order in K. If O is a ℤ-order that is maximal among finite ℤ-orders containing it, then O equals the integral closure of ℤ in K.