English
If a ≠ 0 and the roots of map φ P are x, y, z, then the mapped polynomial equals C(φ a) (X − C x)(X − C y)(X − C z).
Русский
Если a ≠ 0 и корни map φ P равны x, y, z, то отображенный кубический полином выражается как C(φ a) (X − C x)(X − C y)(X − C z).
LaTeX
$$$$\\text{If } a \\neq 0 \\text{ and } (\\mathrm{map}\\;\\varphi\\;P).\\mathrm{roots} = \\{x,y,z\\}, \\text{ then } (\\mathrm{map}\\;\\varphi\\;P).toPoly = C(\\varphi P.a) (X - C x) (X - C y) (X - C z).$$$$
Lean4
theorem eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = { x, y, z }) :
(map φ P).toPoly = C (φ P.a) * (X - C x) * (X - C y) * (X - C z) :=
by
rw [map_toPoly,
eq_prod_roots_of_splits <|
(splits_iff_roots_eq_three ha).mpr <| Exists.intro x <| Exists.intro y <| Exists.intro z h3,
leadingCoeff_of_a_ne_zero ha, ← map_roots, h3]
change C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = _
rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]
