Module

IntegralPrimitiveElement.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.IntegralPrimitiveElement

3 declarations indexed from sourceView source ↗

Module documentation

Integral primitive elements and their finite index

Every number field has an integral primitive element. Its order has full integer rank, so its additive index is nonzero and lies in its conductor. Consequently the exponent used in Kummer--Dedekind is nonzero.

Imports6

Mathlib.FieldTheory.PrimitiveElement
Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Mathlib.RingTheory.Algebraic.Integral
Mathlib.GroupTheory.Index

Imported by2

theorem

exists_integral_primitive_element

L28 ↗

AlgebraicNumberTheory.PrimeSelection.exists_integral_primitive_element

Documentation

A number field has a primitive element in its actual ring of integers.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField Module Polynomial
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem exists_integral_primitive_element
    (K : Type*) [Field K] [NumberField K] :
    ∃ θ : 𝓞 K, IntermediateField.adjoin ℚ ({(θ : K)} : Set K) = ⊤

theorem

integralPrimitiveOrder_finrank

L51 ↗

AlgebraicNumberTheory.PrimeSelection.integralPrimitiveOrder_finrank

Documentation

The order of an integral primitive element has full integer rank.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField Module Polynomial
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem integralPrimitiveOrder_finrank
    (K : Type*) [Field K] [NumberField K]
    (θ : 𝓞 K)
    (hθ : IntermediateField.adjoin ℚ ({(θ : K)} : Set K) = ⊤) :
    Module.finrank ℤ (Algebra.adjoin ℤ ({θ} : Set (𝓞 K))) =
      Module.finrank ℤ (𝓞 K)

theorem

integralPrimitive_exponent_ne_zero

L73 ↗

AlgebraicNumberTheory.PrimeSelection.integralPrimitive_exponent_ne_zero

Documentation

The Kummer--Dedekind exponent of an integral primitive element is nonzero.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField Module Polynomial
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem integralPrimitive_exponent_ne_zero
    (K : Type*) [Field K] [NumberField K]
    (θ : 𝓞 K)
    (hθ : IntermediateField.adjoin ℚ ({(θ : K)} : Set K) = ⊤) :
    RingOfIntegers.exponent θ ≠ 0

Module documentation

Integral primitive elements and their finite index

Declarations

exists_integral_primitive_element

integralPrimitiveOrder_finrank

integralPrimitive_exponent_ne_zero