isRadical

Mathlib.FieldTheory.Minpoly.Field

URI: https://scilib.ai/kg/mathlib#minpoly.isRadical

← MathLib Explorer

English

If the base algebra is reduced, then minpoly is a radical polynomial.

Русский

Если база редуцирована, то minpoly радикальный полином.

LaTeX

$$$\\text{IsRadical}(\\minpoly A x)$$$

Lean4

theorem isRadical [IsReduced B] : IsRadical (minpoly A x) := fun n p dvd ↦ by rw [dvd_iff] at dvd ⊢;
  rw [map_pow] at dvd; exact IsReduced.eq_zero _ ⟨n, dvd⟩

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

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

Разделы

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

Аффилиация

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