# Number fields #

This file defines a number field and the ring of integers corresponding to it.

## Main definitions #

- `NumberField` defines a number field as a field which has characteristic zero and is finite dimensional over ℚ.
- `RingOfIntegers` 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.

## References #

- [D. Marcus, Number Fields][marcus1977number]
- [J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory][cassels1967algebraic]
- [P. Samuel, Algebraic Theory of Numbers][samuel1967]

## Tags #

number field, ring of integers

source
class NumberField (K : Type u_1) [Field K] :
Prop

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

- to_charZero : CharZero K
- to_finiteDimensional : FiniteDimensional ℚ K

Instances

source
theorem Int.not_isField :
¬IsField ℤ

`ℤ` with its usual ring structure is not a field.

source
theorem NumberField.isAlgebraic (K : Type u_1) [Field K] [NumberField K] :
Algebra.IsAlgebraic ℚ K
source
instance NumberField.instFiniteDimensional (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] :
FiniteDimensional K L
source
theorem NumberField.of_module_finite (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [Algebra K L] [Module.Finite K L] :
NumberField L

A finite extension of a number field is a number field.

source
instance NumberField.of_intermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (E : IntermediateField K L) :
NumberField ↥E
source
instance NumberField.of_subfield {K : Type u_1} [Field K] [NumberField K] (E : Subfield K) :
NumberField ↥E
source
theorem NumberField.of_tower (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (E : Type u_3) [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] :
NumberField E
source
theorem NumberField.of_ringEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] (e : K ≃+* L) [NumberField K] :
NumberField L
source
def 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.

Equations

- NumberField.RingOfIntegers K = ↥(integralClosure ℤ K)

Instances For

source
def NumberField.term𝓞 :
Lean.ParserDescr

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.

Equations

- NumberField.term𝓞 = Lean.ParserDescr.node `NumberField.term𝓞 1024 (Lean.ParserDescr.symbol "𝓞")

Instances For

source
instance NumberField.RingOfIntegers.instCommRing (K : Type u_1) [Field K] :
CommRing (RingOfIntegers K)
Equations

- NumberField.RingOfIntegers.instCommRing K = inferInstanceAs (CommRing ↥(integralClosure ℤ K))

source
instance NumberField.RingOfIntegers.instIsDomain (K : Type u_1) [Field K] :
IsDomain (RingOfIntegers K)
source
instance NumberField.RingOfIntegers.instCharZero (K : Type u_1) [Field K] [NumberField K] :
CharZero (RingOfIntegers K)
source
instance NumberField.RingOfIntegers.instAlgebra (K : Type u_1) [Field K] :
Algebra (RingOfIntegers K) K
Equations

- NumberField.RingOfIntegers.instAlgebra K = inferInstanceAs (Algebra (↥(integralClosure ℤ K)) K)

source
instance NumberField.RingOfIntegers.instNoZeroSMulDivisors (K : Type u_1) [Field K] :
NoZeroSMulDivisors (RingOfIntegers K) K
source
instance NumberField.RingOfIntegers.instNontrivial (K : Type u_1) [Field K] :
Nontrivial (RingOfIntegers K)
source
instance NumberField.RingOfIntegers.instAlgebra_1 (K : Type u_1) [Field K] {L : Type u_3} [Ring L] [Algebra K L] :
Algebra (RingOfIntegers K) L
Equations

- NumberField.RingOfIntegers.instAlgebra_1 K = inferInstanceAs (Algebra (↥(integralClosure ℤ K)) L)

source
instance NumberField.RingOfIntegers.instIsScalarTower (K : Type u_1) [Field K] {L : Type u_3} [Ring L] [Algebra K L] :
IsScalarTower (RingOfIntegers K) K L
source
instance NumberField.RingOfIntegers.instMulSemiringAction (K : Type u_1) [Field K] {G : Type u_3} [Group G] [MulSemiringAction G K] :
MulSemiringAction G (RingOfIntegers K)
Equations

- NumberField.RingOfIntegers.instMulSemiringAction K = inferInstanceAs (MulSemiringAction G ↥(integralClosure ℤ K))

source
instance NumberField.RingOfIntegers.instSMulDistribClass (K : Type u_1) [Field K] {G : Type u_3} [Group G] [MulSemiringAction G K] :
SMulDistribClass G (RingOfIntegers K) K
source
@[reducible, inline]
abbrev NumberField.RingOfIntegers.val {K : Type u_1} [Field K] (x : RingOfIntegers K) :
K

The canonical coercion from `𝓞 K` to `K`.

Equations

- ↑x = (algebraMap (NumberField.RingOfIntegers K) K) x

Instances For

source
instance NumberField.RingOfIntegers.instCoeHead {K : Type u_1} [Field K] :
CoeHead (RingOfIntegers K) K

This instance has to be `CoeHead` because we only want to apply it from `𝓞 K` to `K`.

Equations

- NumberField.RingOfIntegers.instCoeHead = { coe := NumberField.RingOfIntegers.val }

source
theorem NumberField.RingOfIntegers.coe_eq_algebraMap {K : Type u_1} [Field K] (x : RingOfIntegers K) :
↑x = (algebraMap (RingOfIntegers K) K) x
source
theorem NumberField.RingOfIntegers.ext {K : Type u_1} [Field K] {x y : RingOfIntegers K} (h : ↑x = ↑y) :
x = y
source
theorem NumberField.RingOfIntegers.ext_iff {K : Type u_1} [Field K] {x y : RingOfIntegers K} :
x = y ↔ ↑x = ↑y
source
theorem NumberField.RingOfIntegers.eq_iff {K : Type u_1} [Field K] {x y : RingOfIntegers K} :
↑x = ↑y ↔ x = y
source
@[simp]
theorem NumberField.RingOfIntegers.map_mk {K : Type u_1} [Field K] (x : K) (hx : x ∈ integralClosure ℤ K) :
(algebraMap (RingOfIntegers K) K) ⟨x, hx⟩ = x
source
theorem NumberField.RingOfIntegers.coe_mk {K : Type u_1} [Field K] {x : K} (hx : x ∈ integralClosure ℤ K) :
↑⟨x, hx⟩ = x
source
theorem NumberField.RingOfIntegers.mk_eq_mk {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) :
⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y
source
@[simp]
theorem NumberField.RingOfIntegers.mk_one {K : Type u_1} [Field K] :
⟨1, ⋯⟩ = 1
source
@[simp]
theorem NumberField.RingOfIntegers.mk_zero {K : Type u_1} [Field K] :
⟨0, ⋯⟩ = 0
source
@[simp]
theorem NumberField.RingOfIntegers.mk_add_mk {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) :
⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
source
@[simp]
theorem NumberField.RingOfIntegers.mk_mul_mk {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) :
⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
source
@[simp]
theorem NumberField.RingOfIntegers.mk_sub_mk {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) :
⟨x, hx⟩ - ⟨y, hy⟩ = ⟨x - y, ⋯⟩
source
@[simp]
theorem NumberField.RingOfIntegers.neg_mk {K : Type u_1} [Field K] (x : K) (hx : x ∈ integralClosure ℤ K) :
-⟨x, hx⟩ = ⟨-x, ⋯⟩
source
def NumberField.RingOfIntegers.mapRingHom {K : Type u_3} {L : Type u_4} [Field K] [Field L] (f : K →+* L) :
RingOfIntegers K →+* RingOfIntegers L

The ring homomorphism `(𝓞 K) →+* (𝓞 L)` given by restricting a ring homomorphism `f : K →+* L` to `𝓞 K`.

Equations

- NumberField.RingOfIntegers.mapRingHom f = { toFun := fun (k : NumberField.RingOfIntegers K) => ⟨f ↑k, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem NumberField.RingOfIntegers.mapRingHom_apply {K : Type u_3} {L : Type u_4} [Field K] [Field L] (f : K →+* L) (x : RingOfIntegers K) :
↑((mapRingHom f) x) = f ↑x
source
def NumberField.RingOfIntegers.mapRingEquiv {K : Type u_3} {L : Type u_4} [Field K] [Field L] (e : K ≃+* L) :
RingOfIntegers K ≃+* RingOfIntegers L

The ring isomorphism `(𝓞 K) ≃+* (𝓞 L)` given by restricting a ring isomorphism `e : K ≃+* L` to `𝓞 K`.

Equations

- NumberField.RingOfIntegers.mapRingEquiv e = RingEquiv.ofRingHom (NumberField.RingOfIntegers.mapRingHom ↑e) (NumberField.RingOfIntegers.mapRingHom ↑e.symm) ⋯ ⋯

Instances For

source
@[simp]
theorem NumberField.RingOfIntegers.mapRingEquiv_apply {K : Type u_3} {L : Type u_4} [Field K] [Field L] (e : K ≃+* L) (x : RingOfIntegers K) :
↑((mapRingEquiv e) x) = e ↑x
source
@[simp]
theorem NumberField.RingOfIntegers.mapRingEquiv_symm_apply {K : Type u_3} {L : Type u_4} [Field K] [Field L] (e : K ≃+* L) (x : RingOfIntegers L) :
↑((mapRingEquiv e).symm x) = e.symm ↑x
source
instance NumberField.inst_ringOfIntegersAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :
Algebra (RingOfIntegers K) (RingOfIntegers L)

Given an algebra structure between two fields, this instance creates an algebra structure between their two rings of integers.

Equations

- NumberField.inst_ringOfIntegersAlgebra K L = (NumberField.RingOfIntegers.mapRingHom (algebraMap K L)).toAlgebra

source
def NumberField.RingOfIntegers.mapAlgHom {k : Type u_3} {K : Type u_4} {L : Type u_5} {F : Type u_6} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [FunLike F K L] [AlgHomClass F k K L] (f : F) :
RingOfIntegers K →ₐ[RingOfIntegers k] RingOfIntegers L

The algebra homomorphism `(𝓞 K) →ₐ[𝓞 k] (𝓞 L)` given by restricting an algebra homomorphism `f : K →ₐ[k] L` to `𝓞 K`.

Equations

- NumberField.RingOfIntegers.mapAlgHom f = { toRingHom := NumberField.RingOfIntegers.mapRingHom ↑f, commutes' := ⋯ }

Instances For

source
def NumberField.RingOfIntegers.mapAlgEquiv {k : Type u_3} {K : Type u_4} {L : Type u_5} {E : Type u_6} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [EquivLike E K L] [AlgEquivClass E k K L] (e : E) :
RingOfIntegers K ≃ₐ[RingOfIntegers k] RingOfIntegers L

The isomorphism of algebras `(𝓞 K) ≃ₐ[𝓞 k] (𝓞 L)` given by restricting an isomorphism of algebras `e : K ≃ₐ[k] L` to `𝓞 K`.

Equations

- NumberField.RingOfIntegers.mapAlgEquiv e = AlgEquiv.ofAlgHom (NumberField.RingOfIntegers.mapAlgHom e) (NumberField.RingOfIntegers.mapAlgHom (↑e).symm) ⋯ ⋯

Instances For

source
instance NumberField.RingOfIntegers.inst_isScalarTower (k : Type u_3) (K : Type u_4) (L : Type u_5) [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [Algebra K L] [IsScalarTower k K L] :
IsScalarTower (RingOfIntegers k) (RingOfIntegers K) (RingOfIntegers L)
source
theorem NumberField.RingOfIntegers.coe_injective {K : Type u_1} [Field K] :
Function.Injective ⇑(algebraMap (RingOfIntegers K) K)

The canonical map from `𝓞 K` to `K` is injective.

This is a convenient abbreviation for `FaithfulSMul.algebraMap_injective`.

source
theorem NumberField.RingOfIntegers.coe_eq_zero_iff {K : Type u_1} [Field K] {x : RingOfIntegers K} :
(algebraMap (RingOfIntegers K) K) x = 0 ↔ x = 0

The canonical map from `𝓞 K` to `K` is injective.

This is a convenient abbreviation for `map_eq_zero_iff` applied to `FaithfulSMul.algebraMap_injective`.

source
theorem NumberField.RingOfIntegers.coe_ne_zero_iff {K : Type u_1} [Field K] {x : RingOfIntegers K} :
(algebraMap (RingOfIntegers K) K) x ≠ 0 ↔ x ≠ 0

The canonical map from `𝓞 K` to `K` is injective.

This is a convenient abbreviation for `map_ne_zero_iff` applied to `FaithfulSMul.algebraMap_injective`.

source
theorem NumberField.RingOfIntegers.isIntegral_coe {K : Type u_1} [Field K] (x : RingOfIntegers K) :
IsIntegral ℤ ((algebraMap (RingOfIntegers K) K) x)
source
theorem NumberField.RingOfIntegers.isIntegral {K : Type u_1} [Field K] (x : RingOfIntegers K) :
IsIntegral ℤ x
source
instance NumberField.RingOfIntegers.instIsFractionRing {K : Type u_1} [Field K] [NumberField K] :
IsFractionRing (RingOfIntegers K) K
source
instance NumberField.RingOfIntegers.instIsIntegralClosureInt {K : Type u_1} [Field K] :
IsIntegralClosure (RingOfIntegers K) ℤ K
source
instance NumberField.RingOfIntegers.instIsIntegralInt {K : Type u_1} [Field K] :
Algebra.IsIntegral ℤ (RingOfIntegers K)
source
instance NumberField.RingOfIntegers.instIsIntegrallyClosed {K : Type u_1} [Field K] [NumberField K] :
IsIntegrallyClosed (RingOfIntegers K)
source
noncomputable def NumberField.RingOfIntegers.equiv {K : Type u_1} [Field K] (R : Type u_3) [CommRing R] [Algebra R K] [IsIntegralClosure R ℤ K] :
RingOfIntegers K ≃+* R

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

Equations

- NumberField.RingOfIntegers.equiv R = (IsIntegralClosure.equiv ℤ R K (NumberField.RingOfIntegers K)).symm.toRingEquiv

Instances For

source
instance NumberField.RingOfIntegers.instCharZero_1 (K : Type u_1) [Field K] [CharZero K] :
CharZero (RingOfIntegers K)
source
instance NumberField.RingOfIntegers.instIsNoetherianInt (K : Type u_1) [Field K] [NumberField K] :
IsNoetherian ℤ (RingOfIntegers K)
source
theorem NumberField.RingOfIntegers.not_isField (K : Type u_1) [Field K] [NumberField K] :
¬IsField (RingOfIntegers K)

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

source
instance NumberField.RingOfIntegers.instIsDedekindDomain (K : Type u_1) [Field K] [NumberField K] :
IsDedekindDomain (RingOfIntegers K)
source
instance NumberField.RingOfIntegers.instFreeInt (K : Type u_1) [Field K] [NumberField K] :
Module.Free ℤ (RingOfIntegers K)
source
instance NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors (K : Type u_1) [Field K] [NumberField K] :
IsLocalization (Algebra.algebraMapSubmonoid (RingOfIntegers K) (nonZeroDivisors ℤ)) K
source
noncomputable def NumberField.RingOfIntegers.basis (K : Type u_1) [Field K] [NumberField K] :
Module.Basis (Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K)) ℤ (RingOfIntegers K)

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

Equations

- NumberField.RingOfIntegers.basis K = Module.Free.chooseBasis ℤ (NumberField.RingOfIntegers K)

Instances For

source
def NumberField.RingOfIntegers.restrict {K : Type u_1} [Field K] {M : Type u_3} (f : M → K) (h : ∀ (x : M), IsIntegral ℤ (f x)) (x : M) :
RingOfIntegers K

Given `f : M → K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function `M → 𝓞 K`.

Equations

- NumberField.RingOfIntegers.restrict f h x = ⟨f x, ⋯⟩

Instances For

source
def NumberField.RingOfIntegers.restrict_addMonoidHom {K : Type u_1} [Field K] {M : Type u_3} [AddZeroClass M] (f : M →+ K) (h : ∀ (x : M), IsIntegral ℤ (f x)) :
M →+ RingOfIntegers K

Given `f : M →+ K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function `M →+ 𝓞 K`.

Equations

- NumberField.RingOfIntegers.restrict_addMonoidHom f h = { toFun := NumberField.RingOfIntegers.restrict (⇑f) h, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
def NumberField.RingOfIntegers.restrict_monoidHom {K : Type u_1} [Field K] {M : Type u_3} [MulOneClass M] (f : M →* K) (h : ∀ (x : M), IsIntegral ℤ (f x)) :
M →* RingOfIntegers K

Given `f : M →* K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function `M →* 𝓞 K`.

Equations

- NumberField.RingOfIntegers.restrict_monoidHom f h = { toFun := NumberField.RingOfIntegers.restrict (⇑f) h, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
instance NumberField.RingOfIntegers.instIsScalarTower_1 (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] :
IsScalarTower (RingOfIntegers K) (RingOfIntegers L) L
source
instance NumberField.RingOfIntegers.instIsIntegralClosure (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] :
IsIntegralClosure (RingOfIntegers L) (RingOfIntegers K) L
source
noncomputable def NumberField.RingOfIntegers.algEquiv (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] (R : Type u_6) [CommRing R] [Algebra (RingOfIntegers K) R] [Algebra R L] [IsScalarTower (RingOfIntegers K) R L] [IsIntegralClosure R (RingOfIntegers K) L] :
RingOfIntegers L ≃ₐ[RingOfIntegers K] R

The ring of integers of `L` is isomorphic to any integral closure of `𝓞 K` in `L`

Equations

- NumberField.RingOfIntegers.algEquiv K L R = (IsIntegralClosure.equiv (NumberField.RingOfIntegers K) R L (NumberField.RingOfIntegers L)).symm

Instances For

source
instance NumberField.RingOfIntegers.extension_algebra_isIntegral (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] :
Algebra.IsIntegral (RingOfIntegers K) (RingOfIntegers L)

Any extension between ring of integers is integral.

source
instance NumberField.RingOfIntegers.extension_isNoetherian (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] :
IsNoetherian (RingOfIntegers K) (RingOfIntegers L)

Any extension between ring of integers of number fields is Noetherian.

source
theorem NumberField.RingOfIntegers.ker_algebraMap_eq_bot (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] :
RingHom.ker (algebraMap (RingOfIntegers K) (RingOfIntegers L)) = ⊥

The kernel of the algebraMap between ring of integers is `⊥`.

source
theorem NumberField.RingOfIntegers.algebraMap.injective (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] :
Function.Injective ⇑(algebraMap (RingOfIntegers K) (RingOfIntegers L))

The algebraMap between ring of integers is injective.

source
instance NumberField.RingOfIntegers.instNoZeroSMulDivisors_1 (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] :
NoZeroSMulDivisors (RingOfIntegers K) (RingOfIntegers L)
source
instance NumberField.RingOfIntegers.instNoZeroSMulDivisors_2 (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] :
NoZeroSMulDivisors (RingOfIntegers K) L
source
noncomputable def NumberField.integralBasis (K : Type u_1) [Field K] [NumberField K] :
Module.Basis (Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K)) ℚ K

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

Equations

- NumberField.integralBasis K = Module.Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) K (NumberField.RingOfIntegers.basis K)

Instances For

source
@[simp]
theorem NumberField.integralBasis_apply (K : Type u_1) [Field K] [NumberField K] (i : Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K)) :
(integralBasis K) i = (algebraMap (RingOfIntegers K) K) ((RingOfIntegers.basis K) i)
source
@[simp]
theorem NumberField.integralBasis_repr_apply (K : Type u_1) [Field K] [NumberField K] (x : RingOfIntegers K) (i : Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K)) :
((integralBasis K).repr ((algebraMap (RingOfIntegers K) K) x)) i = (algebraMap ℤ ℚ) (((RingOfIntegers.basis K).repr x) i)
source
theorem NumberField.mem_span_integralBasis (K : Type u_1) [Field K] [NumberField K] {x : K} :
x ∈ Submodule.span ℤ (Set.range ⇑(integralBasis K)) ↔ x ∈ (algebraMap (RingOfIntegers K) K).range
source
theorem NumberField.RingOfIntegers.rank (K : Type u_1) [Field K] [NumberField K] :
Module.finrank ℤ (RingOfIntegers K) = Module.finrank ℚ K
source
instance Rat.numberField :
NumberField ℚ
source
noncomputable def Rat.ringOfIntegersEquiv :
NumberField.RingOfIntegers ℚ ≃+* ℤ

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

Equations

- Rat.ringOfIntegersEquiv = NumberField.RingOfIntegers.equiv ℤ

Instances For

source
@[simp]
theorem Rat.ringOfIntegersEquiv_apply_coe (z : NumberField.RingOfIntegers ℚ) :
↑(ringOfIntegersEquiv z) = (algebraMap (NumberField.RingOfIntegers ℚ) ℚ) z
source
theorem Rat.ringOfIntegersEquiv_symm_apply_coe (x : ℤ) :
↑(ringOfIntegersEquiv.symm x) = ↑x
source
instance AdjoinRoot.instNumberFieldRat {f : Polynomial ℚ} [hf : Fact (Irreducible f)] :
NumberField (AdjoinRoot f)

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