instFiniteSplittingField

Mathlib.FieldTheory.SplittingField.Construction

URI: https://scilib.ai/kg/mathlib#Polynomial.IsSplittingField.instFiniteSplittingField

English

If K is finite, then the splitting field of f over K is finite over K.

Русский

Если K конечное, то развертывающее поле f над K конечно по размерности.

LaTeX

$$$\text{Finite}_K(\mathrm{SplittingField}(f))$$$

Lean4

instance [Finite K] (f : K[X]) : Finite f.SplittingField :=
  Module.finite_of_finite K

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru