Module

NormalSplittingPolynomial.lean

Nyll.ValuedFieldTheory.Valuation.NormalSplittingPolynomial

1 declaration indexed from sourceView source ↗

Module documentation

Nonzero splitting polynomials for finite normal extensions

A finite normal extension is the splitting field of a nonzero polynomial. If the polynomial supplied by the standard existence theorem is zero, the constant polynomial one has the same empty root set and generates the same extension.

Imports1

Mathlib.FieldTheory.Normal.Basic

Imported by2

theorem

exists_ne_zero_isSplittingField

L21 ↗

Normal.exists_ne_zero_isSplittingField

Documentation

A finite normal extension admits a nonzero splitting polynomial.

Source context 1 command

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

namespace Normal

Lean source · statement

theorem exists_ne_zero_isSplittingField
    (F K : Type*) [Field F] [Field K] [Algebra F K]
    [Normal F K] [FiniteDimensional F K] :
    ∃ f : Polynomial F, f ≠ 0 ∧ Polynomial.IsSplittingField F K f

Module documentation

Nonzero splitting polynomials for finite normal extensions

Declarations

exists_ne_zero_isSplittingField