mathlib documentation

number_theory.number_field

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]
structure number_field (K : Type u_1) [field K] :
Prop

A number field is a field which has characteristic zero and is finite dimensional over ℚ.

Instances
@[protected]
theorem number_field.is_algebraic (K : Type u_1) [field K] [nf : number_field K] :
def number_field.ring_of_integers (K : Type u_1) [field K] :

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

Equations
theorem number_field.mem_ring_of_integers (K : Type u_1) [field K] (x : K) :
@[protected, instance]
def number_field.ring_of_integers_algebra (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] :
Equations
@[protected, instance]
@[protected, instance]
@[protected]
noncomputable def number_field.ring_of_integers.equiv {K : Type u_1} [field K] (R : Type u_2) [comm_ring R] [algebra R K] [is_integral_closure R K] :

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

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def rat.ring_of_integers_equiv  :

The ring of integers of as a number field is just .

Equations