Module

SeparableFactorCoefficients.lean

Nyll.ValuedFieldTheory.Valuation.Completion.SeparableFactorCoefficients

1 declaration indexed from sourceView source ↗

Module documentation

Separable coefficients of monic factors

The roots of a factor of a separable ground-field polynomial belong to the relative separable closure. A monic factor therefore has its coefficients in that closure, even when the ambient field extension is not algebraic.

Imports3

Mathlib.FieldTheory.SeparableClosure
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.Algebra.Polynomial.Splits

Imported by2

theorem

isSeparable_coeff_of_monic_dvd_map

L25 ↗

ValuationTheory.Completion.isSeparable_coeff_of_monic_dvd_map

Documentation

Every coefficient of a monic factor of a separable ground-field polynomial is separable over the ground field.

Source context 2 commands

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

namespace ValuationTheory.Completion
open Polynomial

Lean source · statement

theorem isSeparable_coeff_of_monic_dvd_map
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    {f : K[X]} (hf : f.Separable) {g : L[X]} (hg : g.Monic)
    (hdiv : g ∣ f.map (algebraMap K L)) (i : ℕ) :
    IsSeparable K (g.coeff i)

Module documentation

Separable coefficients of monic factors

Declarations

isSeparable_coeff_of_monic_dvd_map