Number fields #

This file defines a number field and the ring of integers corresponding to it.

Main definitions #

Implementation notes #

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice.

References #

Tags #

number field, ring of integers

class NumberField (K : Type u_1) [Field K] :

A number field is a field which has characteristic zero and is finite dimensional over β„š.


    β„€ with its usual ring structure is not a field.

    The ring of integers (or number ring) corresponding to a number field is the integral closure of β„€ in the number field.

    Instances For
      theorem NumberField.isIntegral_of_mem_ringOfIntegers {K : Type u_3} [Field K] {x : K} (hx : x ∈ NumberField.ringOfIntegers K) :
      IsIntegral β„€ { val := x, property := hx }

      Given an algebra between two fields, create an algebra between their two rings of integers.

      theorem NumberField.RingOfIntegers.map_mem {K : Type u_1} [Field K] {F : Type u_3} {L : Type u_4} [Field L] [CharZero K] [CharZero L] [AlgHomClass F β„š K L] (f : F) (x : { x // x ∈ NumberField.ringOfIntegers K }) :
      noncomputable def NumberField.RingOfIntegers.equiv {K : Type u_1} [Field K] (R : Type u_3) [CommRing R] [Algebra R K] [IsIntegralClosure R β„€ K] :

      The ring of integers of K are equivalent to any integral closure of β„€ in K

      Instances For

        The ring of integers of a number field is not a field.

        A β„€-basis of the ring of integers of K.

        Instances For

          A basis of K over β„š that is also a basis of π“ž K over β„€.

          Instances For

            The ring of integers of β„š as a number field is just β„€.

            Instances For

              The quotient of β„š[X] by the ideal generated by an irreducible polynomial of β„š[X] is a number field.