splits_of_degree_eq_two — Mathlib

English

If f is a polynomial over K with degree 2 and there exists x in L such that eval₂ i x f = 0, then f splits over i.

Русский

Если полином f над K имеет долю 2 и существует x ∈ L с eval₂ i x f = 0, то f распадается через i.

LaTeX

$$$\forall f:K[X],\forall x:L, (f.degree = 2 \land eval_2 i x f = 0) \Rightarrow Splits\, i\, f$$$

Lean4

theorem splits_of_degree_eq_two {f : Polynomial K} {x : L} (h₁ : f.degree = 2) (h₂ : eval₂ i x f = 0) : Splits i f :=
  splits_of_natDegree_eq_two i (natDegree_eq_of_degree_eq_some h₁) h₂

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