Theorems · Theorem · field theory

Cubic.C_mul_prod_X_sub_C_eq

∀ {S : Type u_2} [inst : CommRing S] {w x y z : S},
  Polynomial.C w * (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z) =
    { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly

Defined in

Mathlib.Algebra.CubicDiscriminant

Cited by

2 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing