English
Let P be a cubic polynomial over a field F and φ a field homomorphism F → K. If the leading coefficient a of P is nonzero, the φ-image map (map φ P) has exactly three roots x, y, z in K and the discriminant of P is nonzero, then the root multiset of map φ P consists of three distinct roots; equivalently, the finitary root set has size 3.
Русский
Пусть P — кубический многочлен над полем F и φ — гомоморфизм полей F → K. Если a — старшая коэффициент P не равен нулю, множество корней (map φ P) равно {x, y, z} и дискриминант P не равен нулю, тогда корни являются попарно различными и мощность множества корней равна 3.
LaTeX
$$$(map\\;\\varphi\\;P).roots^{\\,\\mathrm{toFinset}}.card = 3,$ под условием $P.a \\neq 0$, $(map\\;\\varphi\\;P).roots = \\{x, y, z\\}$ и $P.disc \\neq 0$.$$
Lean4
theorem card_roots_of_disc_ne_zero [DecidableEq K] (ha : P.a ≠ 0) (h3 : (map φ P).roots = { x, y, z })
(hd : P.disc ≠ 0) : (map φ P).roots.toFinset.card = 3 :=
by
rw [toFinset_card_of_nodup <| (disc_ne_zero_iff_roots_nodup ha h3).mp hd, ← splits_iff_card_roots ha,
splits_iff_roots_eq_three ha]
exact ⟨x, ⟨y, ⟨z, h3⟩⟩⟩
