splits_iff_card_roots — Mathlib

English

Let a ≠ 0. Splits φ P.toPoly if and only if the mapped roots have cardinality 3.

Русский

Пусть a ≠ 0. Разложение φ P.toPoly эквивалентно тому, что образованные корни имеют кардинал 3.

LaTeX

$$$$\\text{Splits }\\varphi\\,P.toPoly \\iff \\operatorname{card}( (map\\varphi\\,P).roots ) = 3.$$$$

Lean4

theorem splits_iff_card_roots (ha : P.a ≠ 0) : Splits φ P.toPoly ↔ Multiset.card (map φ P).roots = 3 :=
  by
  replace ha : (map φ P).a ≠ 0 := (_root_.map_ne_zero φ).mpr ha
  nth_rw 1 [← RingHom.id_comp φ]
  rw [roots, ← splits_map_iff, ← map_toPoly, Polynomial.splits_iff_card_roots, ←
    ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]

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