Module

NormalCyclotomicTower.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.NormalCyclotomicTower

1 declaration indexed from sourceView source ↗

Module documentation

Cyclotomic extensions above finite normal extensions

Adjoining roots of unity to a finite normal extension preserves normality over the original field. The upper field is the splitting field of the product of a nonzero lower splitting polynomial and X^n - 1.

Imports3

Nyll.ValuedFieldTheory.Valuation.NormalSplittingPolynomial
Mathlib.NumberTheory.Cyclotomic.Basic
Mathlib.FieldTheory.SplittingField.IsSplittingField

Imported by5

theorem

normal_cyclotomic_tower

L25 ↗

ValuationTheory.DiscreteValuationField.normal_cyclotomic_tower

Documentation

A cyclotomic extension above a finite normal extension is normal over the bottom field, with no characteristic or valuation hypothesis.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
open Polynomial

Lean source · statement

theorem normal_cyclotomic_tower
    (F K E : Type*) [Field F] [Field K] [Field E]
    [Algebra F K] [Algebra F E] [Algebra K E] [IsScalarTower F K E]
    [FiniteDimensional F K] [Normal F K]
    (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} K E] : Normal F E

Module documentation

Cyclotomic extensions above finite normal extensions

Declarations

normal_cyclotomic_tower