algebra

Mathlib.FieldTheory.SplittingField.Construction

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

English

There is a canonical K-algebra structure on SplittingFieldAux(n,f).

Русский

Существует каноническая структура K-алгебры на SplittingFieldAux(n,f).

LaTeX

$$$\\text{Algebra }K\\; (\\text{SplittingFieldAux}(n,f))$$$

Lean4

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

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

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

Разделы

Аффилиация

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