CyclotomicField — Mathlib

English

CyclotomicField n K is defined as the splitting field of cyclotomic n K.

Русский

CyclotomicField n K определяется как разворачивающее поле для циклотомического полинома n(K).

LaTeX

$$$\\text{CyclotomicField}(n,K) := (\\text{cyclotomic}(n,K)).SplittingField$$$

Lean4

/-- Given a nonzero `n : ℕ` and a field `K`, we define `CyclotomicField n K` as the
splitting field of `cyclotomic n K`. If `n` is nonzero in `K`, it has
the instance `IsCyclotomicExtension {n} K (CyclotomicField n K)`. -/
def CyclotomicField : Type w :=
  (cyclotomic n K).SplittingField

Похожие утверждения