splittingField — Mathlib

English

The splitting field is an IsSplittingField for the polynomial f over K.

Русский

Поле развёртывания является полем-разделителем для многочлена f над K.

LaTeX

$$$\mathrm{IsSplittingField}(K, \mathrm{SplittingField}(f), f)$$$

Lean4

instance _root_.Polynomial.IsSplittingField.splittingField (f : K[X]) : IsSplittingField K (SplittingField f) f :=
  IsSplittingField.of_algEquiv _ f (algEquivSplittingFieldAux f).symm

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