field

Mathlib.FieldTheory.SplittingField.Construction

URI: https://scilib.ai/kg/mathlib#Polynomial.SplittingFieldAux.field

English

The structure on SplittingFieldAux(n,f) provides a field with the base field K.

Русский

Структура на SplittingFieldAux(n,f) обеспечивает поле над базовым полем K.

LaTeX

$$$\\text{Field}(\\text{SplittingFieldAux}(n,f))$$$

Lean4

instance field (n : ℕ) {K : Type u} [Field K] (f : K[X]) : Field (SplittingFieldAux n f) :=
  (SplittingFieldAuxAux n f).2.1

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

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

Разделы

Аффилиация

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