Documentation

Mathlib.Algebra.CubicDiscriminant

Cubics and discriminants #

This file defines cubic polynomials over a semiring and their discriminants over a splitting field.

Main definitions #

Main statements #

References #

Tags #

cubic, discriminant, polynomial, root

source
structure Cubic (R : Type u_1) :
Type u_1

The structure representing a cubic polynomial.

  • a : R
  • b : R
  • c : R
  • d : R
Instances For
    source
    theorem Cubic.ext {R : Type u_1} {x y : Cubic R} (a : x.a = y.a) (b : x.b = y.b) (c : x.c = y.c) (d : x.d = y.d) :
    x = y
    source
    instance Cubic.instInhabited {R : Type u_1} [Inhabited R] :
    Inhabited (Cubic R)
    Equations
    • Cubic.instInhabited = { default := { a := default, b := default, c := default, d := default } }
    source
    instance Cubic.instZero {R : Type u_1} [Zero R] :
    Zero (Cubic R)
    Equations
    • Cubic.instZero = { zero := { a := 0, b := 0, c := 0, d := 0 } }
    source
    def Cubic.toPoly {R : Type u_1} [Semiring R] (P : Cubic R) :
    Polynomial R

    Convert a cubic polynomial to a polynomial.

    Equations
    • P.toPoly = Polynomial.C P.a * Polynomial.X ^ 3 + Polynomial.C P.b * Polynomial.X ^ 2 + Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
    Instances For
      source
      theorem Cubic.C_mul_prod_X_sub_C_eq {S : Type u_2} [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
      source
      theorem Cubic.prod_X_sub_C_eq {S : Type u_2} [CommRing S] {x y z : S} :
      (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z) = { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly

      Coefficients #

      source
      @[simp]
      theorem Cubic.coeff_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] {n : ℕ} (hn : 3 < n) :
      P.toPoly.coeff n = 0
      source
      @[simp]
      theorem Cubic.coeff_eq_a {R : Type u_1} {P : Cubic R} [Semiring R] :
      P.toPoly.coeff 3 = P.a
      source
      @[simp]
      theorem Cubic.coeff_eq_b {R : Type u_1} {P : Cubic R} [Semiring R] :
      P.toPoly.coeff 2 = P.b
      source
      @[simp]
      theorem Cubic.coeff_eq_c {R : Type u_1} {P : Cubic R} [Semiring R] :
      P.toPoly.coeff 1 = P.c
      source
      @[simp]
      theorem Cubic.coeff_eq_d {R : Type u_1} {P : Cubic R} [Semiring R] :
      P.toPoly.coeff 0 = P.d
      source
      theorem Cubic.a_of_eq {R : Type u_1} {P Q : Cubic R} [Semiring R] (h : P.toPoly = Q.toPoly) :
      P.a = Q.a
      source
      theorem Cubic.b_of_eq {R : Type u_1} {P Q : Cubic R} [Semiring R] (h : P.toPoly = Q.toPoly) :
      P.b = Q.b
      source
      theorem Cubic.c_of_eq {R : Type u_1} {P Q : Cubic R} [Semiring R] (h : P.toPoly = Q.toPoly) :
      P.c = Q.c
      source
      theorem Cubic.d_of_eq {R : Type u_1} {P Q : Cubic R} [Semiring R] (h : P.toPoly = Q.toPoly) :
      P.d = Q.d
      source
      theorem Cubic.toPoly_injective {R : Type u_1} [Semiring R] (P Q : Cubic R) :
      P.toPoly = Q.toPoly ↔ P = Q
      source
      theorem Cubic.of_a_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) :
      P.toPoly = Polynomial.C P.b * Polynomial.X ^ 2 + Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
      source
      theorem Cubic.of_a_eq_zero' {R : Type u_1} {b c d : R} [Semiring R] :
      { a := 0, b := b, c := c, d := d }.toPoly = Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d
      source
      theorem Cubic.of_b_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) :
      P.toPoly = Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
      source
      theorem Cubic.of_b_eq_zero' {R : Type u_1} {c d : R} [Semiring R] :
      { a := 0, b := 0, c := c, d := d }.toPoly = Polynomial.C c * Polynomial.X + Polynomial.C d
      source
      theorem Cubic.of_c_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :
      P.toPoly = Polynomial.C P.d
      source
      theorem Cubic.of_c_eq_zero' {R : Type u_1} {d : R} [Semiring R] :
      { a := 0, b := 0, c := 0, d := d }.toPoly = Polynomial.C d
      source
      theorem Cubic.of_d_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) :
      P.toPoly = 0
      source
      theorem Cubic.of_d_eq_zero' {R : Type u_1} [Semiring R] :
      { a := 0, b := 0, c := 0, d := 0 }.toPoly = 0
      source
      theorem Cubic.zero {R : Type u_1} [Semiring R] :
      Cubic.toPoly 0 = 0
      source
      theorem Cubic.toPoly_eq_zero_iff {R : Type u_1} [Semiring R] (P : Cubic R) :
      P.toPoly = 0 ↔ P = 0
      source
      theorem Cubic.ne_zero_of_a_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) :
      P.toPoly ≠ 0
      source
      theorem Cubic.ne_zero_of_b_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (hb : P.b ≠ 0) :
      P.toPoly ≠ 0
      source
      theorem Cubic.ne_zero_of_c_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (hc : P.c ≠ 0) :
      P.toPoly ≠ 0
      source
      theorem Cubic.ne_zero_of_d_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (hd : P.d ≠ 0) :
      P.toPoly ≠ 0
      source
      @[simp]
      theorem Cubic.leadingCoeff_of_a_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) :
      P.toPoly.leadingCoeff = P.a
      source
      @[simp]
      theorem Cubic.leadingCoeff_of_a_ne_zero' {R : Type u_1} {a b c d : R} [Semiring R] (ha : a ≠ 0) :
      { a := a, b := b, c := c, d := d }.toPoly.leadingCoeff = a
      source
      @[simp]
      theorem Cubic.leadingCoeff_of_b_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b ≠ 0) :
      P.toPoly.leadingCoeff = P.b
      source
      @[simp]
      theorem Cubic.leadingCoeff_of_b_ne_zero' {R : Type u_1} {b c d : R} [Semiring R] (hb : b ≠ 0) :
      { a := 0, b := b, c := c, d := d }.toPoly.leadingCoeff = b
      source
      @[simp]
      theorem Cubic.leadingCoeff_of_c_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) :
      P.toPoly.leadingCoeff = P.c
      source
      @[simp]
      theorem Cubic.leadingCoeff_of_c_ne_zero' {R : Type u_1} {c d : R} [Semiring R] (hc : c ≠ 0) :
      { a := 0, b := 0, c := c, d := d }.toPoly.leadingCoeff = c
      source
      @[simp]
      theorem Cubic.leadingCoeff_of_c_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :
      P.toPoly.leadingCoeff = P.d
      source
      theorem Cubic.leadingCoeff_of_c_eq_zero' {R : Type u_1} {d : R} [Semiring R] :
      { a := 0, b := 0, c := 0, d := d }.toPoly.leadingCoeff = d
      source
      theorem Cubic.monic_of_a_eq_one {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 1) :
      P.toPoly.Monic
      source
      theorem Cubic.monic_of_a_eq_one' {R : Type u_1} {b c d : R} [Semiring R] :
      { a := 1, b := b, c := c, d := d }.toPoly.Monic
      source
      theorem Cubic.monic_of_b_eq_one {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 1) :
      P.toPoly.Monic
      source
      theorem Cubic.monic_of_b_eq_one' {R : Type u_1} {c d : R} [Semiring R] :
      { a := 0, b := 1, c := c, d := d }.toPoly.Monic
      source
      theorem Cubic.monic_of_c_eq_one {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 1) :
      P.toPoly.Monic
      source
      theorem Cubic.monic_of_c_eq_one' {R : Type u_1} {d : R} [Semiring R] :
      { a := 0, b := 0, c := 1, d := d }.toPoly.Monic
      source
      theorem Cubic.monic_of_d_eq_one {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 1) :
      P.toPoly.Monic
      source
      theorem Cubic.monic_of_d_eq_one' :
      { a := 0, b := 0, c := 0, d := 1 }.toPoly.Monic

      Degrees #

      source
      def Cubic.equiv {R : Type u_1} [Semiring R] :
      Cubic R ≃ { p : Polynomial R // p.degree ≤ 3 }

      The equivalence between cubic polynomials and polynomials of degree at most three.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Cubic.equiv_symm_apply_a {R : Type u_1} [Semiring R] (f : { p : Polynomial R // p.degree ≤ 3 }) :
        (Cubic.equiv.symm f).a = (↑f).coeff 3
        source
        @[simp]
        theorem Cubic.equiv_symm_apply_c {R : Type u_1} [Semiring R] (f : { p : Polynomial R // p.degree ≤ 3 }) :
        (Cubic.equiv.symm f).c = (↑f).coeff 1
        source
        @[simp]
        theorem Cubic.equiv_symm_apply_d {R : Type u_1} [Semiring R] (f : { p : Polynomial R // p.degree ≤ 3 }) :
        (Cubic.equiv.symm f).d = (↑f).coeff 0
        source
        @[simp]
        theorem Cubic.equiv_symm_apply_b {R : Type u_1} [Semiring R] (f : { p : Polynomial R // p.degree ≤ 3 }) :
        (Cubic.equiv.symm f).b = (↑f).coeff 2
        source
        @[simp]
        theorem Cubic.equiv_apply_coe {R : Type u_1} [Semiring R] (P : Cubic R) :
        ↑(Cubic.equiv P) = P.toPoly
        source
        @[simp]
        theorem Cubic.degree_of_a_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) :
        P.toPoly.degree = 3
        source
        @[simp]
        theorem Cubic.degree_of_a_ne_zero' {R : Type u_1} {a b c d : R} [Semiring R] (ha : a ≠ 0) :
        { a := a, b := b, c := c, d := d }.toPoly.degree = 3
        source
        theorem Cubic.degree_of_a_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) :
        P.toPoly.degree ≤ 2
        source
        theorem Cubic.degree_of_a_eq_zero' {R : Type u_1} {b c d : R} [Semiring R] :
        { a := 0, b := b, c := c, d := d }.toPoly.degree ≤ 2
        source
        @[simp]
        theorem Cubic.degree_of_b_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b ≠ 0) :
        P.toPoly.degree = 2
        source
        @[simp]
        theorem Cubic.degree_of_b_ne_zero' {R : Type u_1} {b c d : R} [Semiring R] (hb : b ≠ 0) :
        { a := 0, b := b, c := c, d := d }.toPoly.degree = 2
        source
        theorem Cubic.degree_of_b_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) :
        P.toPoly.degree ≤ 1
        source
        theorem Cubic.degree_of_b_eq_zero' {R : Type u_1} {c d : R} [Semiring R] :
        { a := 0, b := 0, c := c, d := d }.toPoly.degree ≤ 1
        source
        @[simp]
        theorem Cubic.degree_of_c_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) :
        P.toPoly.degree = 1
        source
        @[simp]
        theorem Cubic.degree_of_c_ne_zero' {R : Type u_1} {c d : R} [Semiring R] (hc : c ≠ 0) :
        { a := 0, b := 0, c := c, d := d }.toPoly.degree = 1
        source
        theorem Cubic.degree_of_c_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :
        P.toPoly.degree ≤ 0
        source
        theorem Cubic.degree_of_c_eq_zero' {R : Type u_1} {d : R} [Semiring R] :
        { a := 0, b := 0, c := 0, d := d }.toPoly.degree ≤ 0
        source
        @[simp]
        theorem Cubic.degree_of_d_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d ≠ 0) :
        P.toPoly.degree = 0
        source
        @[simp]
        theorem Cubic.degree_of_d_ne_zero' {R : Type u_1} {d : R} [Semiring R] (hd : d ≠ 0) :
        { a := 0, b := 0, c := 0, d := d }.toPoly.degree = 0
        source
        @[simp]
        theorem Cubic.degree_of_d_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) :
        P.toPoly.degree = ⊥
        source
        theorem Cubic.degree_of_d_eq_zero' {R : Type u_1} [Semiring R] :
        { a := 0, b := 0, c := 0, d := 0 }.toPoly.degree = ⊥
        source
        @[simp]
        theorem Cubic.degree_of_zero {R : Type u_1} [Semiring R] :
        (Cubic.toPoly 0).degree = ⊥
        source
        @[simp]
        theorem Cubic.natDegree_of_a_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) :
        P.toPoly.natDegree = 3
        source
        @[simp]
        theorem Cubic.natDegree_of_a_ne_zero' {R : Type u_1} {a b c d : R} [Semiring R] (ha : a ≠ 0) :
        { a := a, b := b, c := c, d := d }.toPoly.natDegree = 3
        source
        theorem Cubic.natDegree_of_a_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) :
        P.toPoly.natDegree ≤ 2
        source
        theorem Cubic.natDegree_of_a_eq_zero' {R : Type u_1} {b c d : R} [Semiring R] :
        { a := 0, b := b, c := c, d := d }.toPoly.natDegree ≤ 2
        source
        @[simp]
        theorem Cubic.natDegree_of_b_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b ≠ 0) :
        P.toPoly.natDegree = 2
        source
        @[simp]
        theorem Cubic.natDegree_of_b_ne_zero' {R : Type u_1} {b c d : R} [Semiring R] (hb : b ≠ 0) :
        { a := 0, b := b, c := c, d := d }.toPoly.natDegree = 2
        source
        theorem Cubic.natDegree_of_b_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) :
        P.toPoly.natDegree ≤ 1
        source
        theorem Cubic.natDegree_of_b_eq_zero' {R : Type u_1} {c d : R} [Semiring R] :
        { a := 0, b := 0, c := c, d := d }.toPoly.natDegree ≤ 1
        source
        @[simp]
        theorem Cubic.natDegree_of_c_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) :
        P.toPoly.natDegree = 1
        source
        @[simp]
        theorem Cubic.natDegree_of_c_ne_zero' {R : Type u_1} {c d : R} [Semiring R] (hc : c ≠ 0) :
        { a := 0, b := 0, c := c, d := d }.toPoly.natDegree = 1
        source
        @[simp]
        theorem Cubic.natDegree_of_c_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :
        P.toPoly.natDegree = 0
        source
        theorem Cubic.natDegree_of_c_eq_zero' {R : Type u_1} {d : R} [Semiring R] :
        { a := 0, b := 0, c := 0, d := d }.toPoly.natDegree = 0
        source
        @[simp]
        theorem Cubic.natDegree_of_zero {R : Type u_1} [Semiring R] :
        (Cubic.toPoly 0).natDegree = 0

        Map across a homomorphism #

        source
        def Cubic.map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (φ : R →+* S) (P : Cubic R) :
        Cubic S

        Map a cubic polynomial across a semiring homomorphism.

        Equations
        • Cubic.map φ P = { a := φ P.a, b := φ P.b, c := φ P.c, d := φ P.d }
        Instances For
          source
          theorem Cubic.map_toPoly {R : Type u_1} {S : Type u_2} {P : Cubic R} [Semiring R] [Semiring S] {φ : R →+* S} :
          (Cubic.map φ P).toPoly = Polynomial.map φ P.toPoly

          Roots over an extension #

          source
          def Cubic.roots {R : Type u_1} [CommRing R] [IsDomain R] (P : Cubic R) :
          Multiset R

          The roots of a cubic polynomial.

          Equations
          • P.roots = P.toPoly.roots
          Instances For
            source
            theorem Cubic.map_roots {R : Type u_1} {S : Type u_2} {P : Cubic R} [CommRing R] [CommRing S] {φ : R →+* S} [IsDomain S] :
            (Cubic.map φ P).roots = (Polynomial.map φ P.toPoly).roots
            source
            theorem Cubic.mem_roots_iff {R : Type u_1} {P : Cubic R} [CommRing R] [IsDomain R] (h0 : P.toPoly ≠ 0) (x : R) :
            x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
            source
            theorem Cubic.card_roots_le {R : Type u_1} {P : Cubic R} [CommRing R] [IsDomain R] [DecidableEq R] :
            P.roots.toFinset.card ≤ 3

            Roots over a splitting field #

            source
            theorem Cubic.splits_iff_card_roots {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) :
            Polynomial.Splits φ P.toPoly ↔ (Cubic.map φ P).roots.card = 3
            source
            theorem Cubic.splits_iff_roots_eq_three {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) :
            Polynomial.Splits φ P.toPoly ↔ ∃ (x : K) (y : K) (z : K), (Cubic.map φ P).roots = {x, y, z}
            source
            theorem Cubic.eq_prod_three_roots {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) :
            (Cubic.map φ P).toPoly = Polynomial.C (φ P.a) * (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z)
            source
            theorem Cubic.eq_sum_three_roots {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) :
            Cubic.map φ P = { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }
            source
            theorem Cubic.b_eq_three_roots {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) :
            φ P.b = φ P.a * -(x + y + z)
            source
            theorem Cubic.c_eq_three_roots {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) :
            φ P.c = φ P.a * (x * y + x * z + y * z)
            source
            theorem Cubic.d_eq_three_roots {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) :
            φ P.d = φ P.a * -(x * y * z)

            Discriminant over a splitting field #

            source
            def Cubic.disc {R : Type u_5} [Ring R] (P : Cubic R) :
            R

            The discriminant of a cubic polynomial.

            Equations
            • P.disc = P.b ^ 2 * P.c ^ 2 - 4 * P.a * P.c ^ 3 - 4 * P.b ^ 3 * P.d - 27 * P.a ^ 2 * P.d ^ 2 + 18 * P.a * P.b * P.c * P.d
            Instances For
              source
              theorem Cubic.disc_eq_prod_three_roots {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) :
              φ P.disc = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
              source
              theorem Cubic.disc_ne_zero_iff_roots_ne {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) :
              P.disc ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
              source
              theorem Cubic.disc_ne_zero_iff_roots_nodup {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) :
              P.disc ≠ 0 ↔ (Cubic.map φ P).roots.Nodup
              source
              theorem Cubic.card_roots_of_disc_ne_zero {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} [DecidableEq K] (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) (hd : P.disc ≠ 0) :
              (Cubic.map φ P).roots.toFinset.card = 3