minpolyDiv_monic

Mathlib.FieldTheory.Minpoly.MinpolyDiv

URI: https://scilib.ai/kg/mathlib#minpolyDiv_monic

← MathLib Explorer

English

If hx holds, then minpolyDiv R x is monic.

Русский

Если выполняется hx, то minpolyDiv R x мономиален.

LaTeX

$$Monic (minpolyDiv R x)$$

Lean4

theorem minpolyDiv_monic : Monic (minpolyDiv R x) :=
  by
  nontriviality S
  have := congr_arg leadingCoeff (minpolyDiv_spec R x)
  rw [leadingCoeff_mul', ((minpoly.monic hx).map (algebraMap R S)).leadingCoeff] at this
  · simpa using this
  · simpa using minpolyDiv_ne_zero hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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