splits_iff_card_roots — Mathlib

English

A polynomial splits over RingHom.id if and only if the number of its roots equals its degree.

Русский

Полином распадается над RingHom.id тогда и только тогда, когда число корней равно степеням полинома.

LaTeX

$$$Splits\ RingHom.id\ K p \iff |p.roots| = p.natDegree$$$

Lean4

/-- A polynomial splits if and only if it has as many roots as its degree. -/
theorem splits_iff_card_roots {p : K[X]} : Splits (RingHom.id K) p ↔ Multiset.card p.roots = p.natDegree :=
  by
  constructor
  · intro H
    rw [natDegree_eq_card_roots H, map_id]
  · intro hroots
    rw [splits_iff_exists_multiset (RingHom.id K)]
    use p.roots
    simp only [RingHom.id_apply, map_id]
    exact (C_leadingCoeff_mul_prod_multiset_X_sub_C hroots).symm

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