splits_iff_roots_eq_three — Mathlib

English

If a ≠ 0, Splits φ P.toPoly is equivalent to the existence of three roots x, y, z with map φ P roots = {x, y, z}.

Русский

Если a ≠ 0, разложение φ P.toPoly эквивалентно существованию трех корней x, y, z с равенством map φ P roots = {x, y, z}.

LaTeX

$$$$\\text{Splits }\\varphi\\,P.toPoly \\iff \\exists x,y,z:\\ K, (map \\varphi\\,P).roots = \\{x,y,z\\}.$$$$

Lean4

theorem splits_iff_roots_eq_three (ha : P.a ≠ 0) : Splits φ P.toPoly ↔ ∃ x y z : K, (map φ P).roots = { x, y, z } := by
  rw [splits_iff_card_roots ha, card_eq_three]

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