Theorems · Theorem · field theory

Cubic.discr_ne_zero_iff_roots_ne

∀ {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 ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z)

Defined in

Mathlib.Algebra.CubicDiscriminant

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldField