mathlib3 documentation

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 #

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 of this typeclass

with its usual ring structure is not a field.

@[protected]

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]

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

Equations

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

@[protected, instance]

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.