Theorems · Theorem · field theory

Cubic.discr_eq_prod_three_roots

∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
  P.a ≠ 0 → (Cubic.map φ P).roots = {x, y, z} → φ P.discr = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Defined in

Mathlib.Algebra.CubicDiscriminant

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldField