splits_X_sub_C — Mathlib

English

Let i: K → L be a ring hom between a commutative ring K and a field L. For every x ∈ K, the polynomial X − C x (i.e. X minus the constant C x) splits in L[X] after applying i to the coefficients.

Русский

Пусть i: K → L — эмфеморфизм колец, где K — коммутативное кольцо, L — поле. Для каждого x ∈ K полином X − C x (в L[X], коэффициенты получаются через i) раскладывается на линейные множители.

LaTeX

$$$\forall x \in K,\ (X - C x) \text{ splits in } L[X]$$$

Lean4

theorem splits_X_sub_C {x : K} : (X - C x).Splits i :=
  splits_of_degree_le_one _ <| degree_X_sub_C_le _

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