splits_iff_exists_multiset — Mathlib

English

A polynomial f splits over i if and only if there exists a multiset s of L such that f.map i equals C (i f.leadingCoeff) times the product over (X - C a) for a in s.

Русский

Полином f распадается через i тогда и только тогда, когда существует мультисет s таких элементов L, что f.map i = C(i leadingCoeff)·∏_{a∈s}(X - C a).

LaTeX

$$$Splits\ i\ f \iff \exists s:Multiset\ L,\ f.map\ i = C(i f.leadingCoeff) \cdot (s.map (\lambda a. X - C a)).prod$$$

Lean4

theorem splits_iff_exists_multiset {f : K[X]} :
    Splits i f ↔ ∃ s : Multiset L, f.map i = C (i f.leadingCoeff) * (s.map fun a : L => X - C a).prod :=
  ⟨fun hf => ⟨(f.map i).roots, eq_prod_roots_of_splits hf⟩, fun ⟨_, hs⟩ => splits_of_exists_multiset i hs⟩

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