monic

Mathlib.FieldTheory.Fixed

URI: https://scilib.ai/kg/mathlib#FixedPoints.minpoly.monic

English

The minimal polynomial minpoly G F x is monic as a polynomial over the fixed-point subfield.

Русский

Минимальный полином minpoly G F x моничен как многочлен над фиксированным подполем.

LaTeX

$$$ \\text{monic} (\\mathrm{minpoly}\\,G\\,F\\,x) $$$

Lean4

theorem monic : (minpoly G F x).Monic := by
  simp only [minpoly]
  rw [Polynomial.monic_toSubring]
  exact prodXSubSMul.monic G F x

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

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

Разделы

Аффилиация

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