# mathlib3documentation

number_theory.number_field.basic

# Number fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines a number field and the ring of integers corresponding to it.

## Main definitions #

• number_field defines a number field as a field which has characteristic zero and is finite dimensional over ℚ.
• ring_of_integers defines the ring of integers (or number ring) corresponding to a number field as the integral closure of ℤ in the number field.

## Implementation notes #

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

## Tags #

number field, ring of integers

@[class]
structure number_field (K : Type u_1) [field K] :
Prop
• to_char_zero :
• to_finite_dimensional :

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

Instances of this typeclass
theorem int.not_is_field  :

ℤ with its usual ring structure is not a field.

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

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

Equations
Instances for ↥number_field.ring_of_integers
theorem number_field.mem_ring_of_integers (K : Type u_1) [field K] (x : K) :
theorem number_field.is_integral_of_mem_ring_of_integers {K : Type u_1} [field K] {x : K} (hx : x ) :
x, hx⟩
def number_field.ring_of_integers_algebra (K : Type u_1) (L : Type u_2) [field K] [field L] [ L] :

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

For now, this is not an instance by default as it creates an equal-but-not-defeq diamond with algebra.id when K = L. This is caused by x = ⟨x, x.prop⟩ not being defeq on subtypes. This will likely change in Lean 4.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem number_field.ring_of_integers.map_mem {K : Type u_1} [field K] {F : Type u_2} {L : Type u_3} [field L] [char_zero K] [char_zero L] [ K L] (f : F) (x : ) :
@[protected]
noncomputable def number_field.ring_of_integers.equiv {K : Type u_1} [field K] (R : Type u_2) [comm_ring R] [ K] [ K] :

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

Equations
@[protected, instance]
@[protected, instance]

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def number_field.ring_of_integers.basis (K : Type u_1) [field K] [nf : number_field K] :

A ℤ-basis of the ring of integers of K.

Equations
noncomputable def number_field.integral_basis (K : Type u_1) [field K] [nf : number_field K] :

A basis of K over ℚ that is also a basis of 𝓞 K over ℤ.

Equations
@[simp]
theorem number_field.integral_basis_apply (K : Type u_1) [field K] [nf : number_field K]  :
@[protected, instance]
noncomputable def rat.ring_of_integers_equiv  :

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

Equations
@[protected, instance]

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