Theorems · Theorem · field theory

Cubic.d_eq_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.d = φ P.a * -(x * y * z)

Defined in

Mathlib.Algebra.CubicDiscriminant

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldField