Module

ArtinSchreierIntegralRoot.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ArtinSchreierIntegralRoot

1 declaration indexed from sourceView source ↗

Module documentation

The integral minimal polynomial of the actual reciprocal root

The standard AdjoinRoot of the fraction-field Eisenstein polynomial already has its canonical coefficient-ring algebra. Its root is integral because it annihilates the displayed monic coefficient-ring polynomial. Comparing minimal polynomials through the fraction field identifies its integral minimal polynomial with that polynomial, without any valuation or Henselianity assumption.

Imports5

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ArtinSchreierEisenstein
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.FieldTheory.Minpoly.Field
Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Mathlib.RingTheory.AdjoinRoot

Imported by1

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.All

theorem

minpoly_artinSchreierAdjoinRoot

L34 ↗

ValuationTheory.DiscreteValuationField.minpoly_artinSchreierAdjoinRoot

Documentation

The actual adjoined reciprocal root has the displayed integral minimal polynomial. Irreducibility and the root equation are constructed here.

Source context 4 commands

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

namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u v

Lean source · statement

theorem minpoly_artinSchreierAdjoinRoot
    (R : Type u) (K : Type v)
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    (π : R) (hπ : Prime π) (n : ℕ) (hn : 1 < n) :
    minpoly R
      (AdjoinRoot.root
        ((artinSchreierInversePolynomial π n).map (algebraMap R K))) =
      artinSchreierInversePolynomial π n

Module documentation

The integral minimal polynomial of the actual reciprocal root

Declarations

minpoly_artinSchreierAdjoinRoot