Theorems · Definition · number theory

NumberField.RingOfIntegers

(K : Type u_1) → [Field K] → Type u_1

The ring of integers (or number ring) corresponding to a number field is the integral closure of ℤ in the number field. This is defined as its own type, rather than a Subalgebra, for performance reasons: looking for instances of the form SMul (RingOfIntegers _) (RingOfIntegers _) makes much more effective use of the discrimination tree than instances of the form SMul (Subtype _) (Subtype _). The drawback is we have to copy over instances manually.

Defined in

Mathlib.NumberTheory.NumberField.Basic

Cited by

413 results in Mathlib

Foundations

Depth 136 from the axioms, rests on 4,382 definitions · uses propext, Classical.choice, Quot.sound

Assumes

Field