minpolyDiv_ne_zero

Mathlib.FieldTheory.Minpoly.MinpolyDiv

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

← MathLib Explorer

English

If x is integral over R, then minpolyDiv R x ≠ 0, provided S is nontrivial.

Русский

Если x интегральна над R, то minpolyDiv R x ≠ 0 при условии, что S не тривиален.

LaTeX

$$minpolyDiv_ne_zero$$

Lean4

theorem minpolyDiv_ne_zero [Nontrivial S] : minpolyDiv R x ≠ 0 :=
  by
  intro e
  have := minpolyDiv_spec R x
  rw [e, zero_mul] at this
  exact ((minpoly.monic hx).map (algebraMap R S)).ne_zero this.symm

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

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

Разделы

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

Аффилиация

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