English
Let f be a polynomial over a field K of natDegree 2. If there exists an element x in L such that evaluating f at x via the ring hom i gives 0, then f splits over i (i.e., f factors completely into linear factors after applying i).
Русский
Пусть f ∈ K[X] имеет natDegree(f) = 2. Тогда если существует x ∈ L such that eval₂ i x f = 0, то f распадается через i на линейные множители.
LaTeX
$$$\forall f:K[X],\forall x:L, (f.natDegree = 2 \land eval_2\, i\, x\, f = 0) \Rightarrow Splits\, i\, f$$$
Lean4
/-- A polynomial of degree `2` with a root splits.
-/
theorem splits_of_natDegree_eq_two {f : Polynomial K} {x : L} (h₁ : f.natDegree = 2) (h₂ : eval₂ i x f = 0) :
Splits i f := by
have hf₀ : f ≠ 0 := ne_zero_of_natDegree_gt (h₁ ▸ zero_lt_two)
have h : (map i f /ₘ (X - C x)).natDegree = 1 := by
rw [natDegree_divByMonic _ (monic_X_sub_C x), natDegree_map, h₁, natDegree_X_sub_C]
replace h₂ := (mem_roots'.mp <| (mem_roots_map_of_injective i.injective hf₀).mpr h₂).2
rw [← splits_id_iff_splits, ← mul_divByMonic_eq_iff_isRoot.mpr h₂]
exact
(splits_mul_iff _ (X_sub_C_ne_zero x) (by simp [ne_zero_of_natDegree_gt, h])).mpr
⟨splits_X_sub_C _, splits_of_natDegree_le_one (RingHom.id L) (by rw [h])⟩
