prod_X_sub_C_eq — Mathlib

English

For x,y,z in a commutative ring S, the product (X − C x)(X − C y)(X − C z) equals the polynomial with coefficients a = 1, b = −(x+y+z), c = xy+xz+yz, d = −xyz.

Русский

Для x,y,z в кольце S произведение (X − C x)(X − C y)(X − C z) равно полиному с коэффициентами a = 1, b = −(x+y+z), c = xy+xz+yz, d = −xyz.

LaTeX

$$$ (X - C x)(X - C y)(X - C z) = \\text{toPoly} \\langle 1, -(x+y+z), x y + x z + y z, -(x y z) \\rangle $$$

Lean4

theorem prod_X_sub_C_eq [CommRing S] {x y z : S} :
    (X - C x) * (X - C y) * (X - C z) = toPoly ⟨1, -(x + y + z), x * y + x * z + y * z, -(x * y * z)⟩ := by
  rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]

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