Orders in number fields

TheoremOrders lie in the ring of integers#✓fully proved

Let \(K\) be a number field and \(O\) an order in \(K\), that is, a subring of \(K\) contained in the ring of integers \(\mathcal{O}_K\) (the integral closure of \(\mathbb{Z}\) in \(K\)) whose field of fractions is \(K\). Then \(O \subseteq \mathcal{O}_K\).

theorem le_integralClosure (h : NumberField.IsOrder K O) :
    O ≤ integralClosure ℤ K

TheoremThe fraction field of an order#✓fully proved

Let \(K\) be a number field and \(O\) an order in \(K\), that is, a subring of \(K\) contained in the ring of integers \(\mathcal{O}_K\) (the integral closure of \(\mathbb{Z}\) in \(K\)) whose field of fractions is \(K\). Then \(K\), with the inclusion \(O \subseteq K\), is a field of fractions of \(O\).

theorem isFractionRing (h : NumberField.IsOrder K O) :
    IsFractionRing O K

Used by 1

Used byElements of a number field are quotients of elements of an order

TheoremElements of a number field are quotients of elements of an order#✓fully proved

Let \(K\) be a number field and \(O\) an order in \(K\), that is, a subring of \(K\) contained in the ring of integers \(\mathcal{O}_K\) (the integral closure of \(\mathbb{Z}\) in \(K\)) whose field of fractions is \(K\). Then for every \(x \in K\) there are \(a, b \in O\) with \(b \neq 0\) and \(x = a / b\).

theorem exists_div_eq (hO : NumberField.IsOrder K O) (x : K) :
    ∃ (a b : O), b ≠ 0 ∧ (a : K) / (b : K) = x

Uses 1

Proof usesThe fraction field of an order

TheoremThe ring of integers is an order#✓fully proved

For every number field \(K\), the ring of integers \(\mathcal{O}_K\), the integral closure of \(\mathbb{Z}\) in \(K\), is an order in \(K\), that is, a subring of \(K\) contained in \(\mathcal{O}_K\) whose field of fractions is \(K\).

theorem NumberField.isOrder_integralClosure (K : Type*) [Field K] [NumberField K] :
    NumberField.IsOrder K (integralClosure ℤ K)

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.