Theorems · Theorem · number theory

IsCyclotomicExtension.isSplittingField_X_pow_sub_one

∀ (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension {n} K L], Polynomial.IsSplittingField K L (Polynomial.X ^ n - 1)

If IsCyclotomicExtension {n} K L, then L is the splitting field of X ^ n - 1.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

0 results in Mathlib

Foundations

Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZeroFieldFieldAlgebraIsCyclotomicExtension