C_mul_prod_X_sub_C_eq — Mathlib

English

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

Русский

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

LaTeX

$$$ C w (X - C x)(X - C y)(X - C z) = C w X^3 - w(x+y+z) X^2 + w(xy+xz+yz) X - wxyz $$$

Lean4

theorem C_mul_prod_X_sub_C_eq [CommRing S] {w x y z : S} :
    C w * (X - C x) * (X - C y) * (X - C z) =
      toPoly ⟨w, w * -(x + y + z), w * (x * y + x * z + y * z), w * -(x * y * z)⟩ :=
  by
  simp only [toPoly, C_neg, C_add, C_mul]
  ring1

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