eq_sum_three_roots — Mathlib

English

If a ≠ 0 and the mapped roots are x, y, z, then map φ P has coefficients a, −a(x+y+z), a(xy+xz+yz), −a xyz.

Русский

Если a ≠ 0 и корни map φ P равны x, y, z, то коэффициенты map φ P заданы как a, −a(x+y+z), a(xy+xz+yz), −a xyz.

LaTeX

$$$$\\mathrm{map}\\;\\varphi\\;P = \\langle \\varphi P.a,\\; -\\varphi P.a (x+y+z),\\; \\varphi P.a (xy+xz+yz),\\; -\\varphi P.a (xyz) \\rangle.$$$$

Lean4

theorem eq_sum_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = { x, y, z }) :
    map φ P = ⟨φ P.a, φ P.a * -(x + y + z), φ P.a * (x * y + x * z + y * z), φ P.a * -(x * y * z)⟩ :=
  by
  apply_fun @toPoly _ _
  · rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]
  · exact fun P Q ↦ (toPoly_injective P Q).mp

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