@[reducible, inline]

abbrev AlgebraicNumber.IsAlgebraicNumber (α : ℂ) : Prop

A complex number is an algebraic number if it is algebraic over the rationals ℚ.

@[reducible, inline]

abbrev AlgebraicNumber.IsAlgebraicInteger (α : ℂ) : Prop

A complex number is an algebraic integer if it is integral over ℤ, i.e. it is the root of a monic polynomial with integer coefficients.

@[simp]

theorem AlgebraicNumber.isAlgebraicNumber_iff (α : ℂ) : IsAlgebraicNumber α ↔ IsAlgebraic ℚ α

Unfolds the definition of IsAlgebraicNumber as algebraicity over ℚ.

@[simp]

theorem AlgebraicNumber.isAlgebraicInteger_iff (α : ℂ) : IsAlgebraicInteger α ↔ IsIntegral ℤ α

Unfolds the definition of IsAlgebraicInteger as integrality over ℤ.

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

Any finite ℤ-subalgebra O of a number field K is contained in the integral closure of ℤ in K, i.e. in the ring of integers 𝓞 K. This expresses that the ring of integers is the maximal order in K.

noncomputable def AlgebraicNumber.ringOfIntegers_unique (K : Type u_1) [Field K] [NumberField K] (R : Type u_2) [CommRing R] [Algebra R K] [IsIntegralClosure R ℤ K] : NumberField.RingOfIntegers K ≃+* R

The ring of integers 𝓞 K of a number field K is unique up to ring isomorphism: any other integral closure R of ℤ in K is canonically isomorphic to 𝓞 K.