comp_X_sub_C — Mathlib

English

If a polynomial f over K[X] splits over L via i, then the polynomial obtained by substituting X with X − a also splits over L via i for any a ∈ K.

Русский

Если многочлен f над K[X] распадается над L через i, то полином, полученный заменой X на X − a, также распадается над L через i для любого a ∈ K.

LaTeX

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

Lean4

theorem comp_X_sub_C (a : K) {f : K[X]} (h : f.Splits i) : (f.comp (X - C a)).Splits i :=
  Splits.comp_of_degree_le_one (degree_X_sub_C_le _) h

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