comp_X_add_C — Mathlib

English

If f splits over i, then the polynomial f with X replaced by X + a also splits over i for any a ∈ K.

Русский

Если f распадается над i, то f( X + a ) распадается над i для любого a ∈ K.

LaTeX

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

Lean4

theorem comp_X_add_C (a : K) {f : K[X]} (h : f.Splits i) : (f.comp (X + C a)).Splits i :=
  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (-a)) h

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