splits — Mathlib

English

For any polynomial f over K, SplittingField f is a splitting field of f over K.

Русский

Для любого многочлена f над K разложение f в поле развёртывания является разложением f над K.

LaTeX

$$$\mathrm{Splits}(\mathrm{algebraMap} K, \mathrm{SplittingField}(f))\, f$$$

Lean4

@[stacks 09HU "Splitting part"]
protected theorem splits : Splits (algebraMap K (SplittingField f)) f :=
  IsSplittingField.splits f.SplittingField f

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