comp_neg_X

Mathlib.Algebra.Polynomial.Splits

URI: https://scilib.ai/kg/mathlib#Polynomial.Splits.comp_neg_X

← MathLib Explorer

English

If f splits over i, then the polynomial f with X replaced by −X also splits over i.

Русский

Если f распадается над i, то f(−X) распадается над i.

LaTeX

$$$\operatorname{Splits}_i(f) \Rightarrow \operatorname{Splits}_i\big(f\circ (-X)\big)$$$

Lean4

theorem comp_neg_X {f : K[X]} (h : f.Splits i) : (f.comp (-X)).Splits i :=
  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (0 : K)) h

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

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

Разделы

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

Аффилиация

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