# Documentation

Mathlib.Algebra.CubicDiscriminant

# Cubics and discriminants #

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

## Main definitions #

• Cubic: the structure representing a cubic polynomial.
• Cubic.disc: the discriminant of a cubic polynomial.

## Main statements #

• Cubic.disc_ne_zero_iff_roots_nodup: the cubic discriminant is not equal to zero if and only if the cubic has no duplicate roots.

## References #

• https://en.wikipedia.org/wiki/Cubic_equation
• https://en.wikipedia.org/wiki/Discriminant

## Tags #

cubic, discriminant, polynomial, root

theorem Cubic.ext {R : Type u_1} (x : ) (y : ) (a : x.a = y.a) (b : x.b = y.b) (c : x.c = y.c) (d : x.d = y.d) :
x = y
theorem Cubic.ext_iff {R : Type u_1} (x : ) (y : ) :
x = y x.a = y.a x.b = y.b x.c = y.c x.d = y.d
structure Cubic (R : Type u_1) :
Type u_1
• a : R
• b : R
• c : R
• d : R

The structure representing a cubic polynomial.

Instances For
instance Cubic.instZeroCubic {R : Type u_1} [Zero R] :
Zero ()
def Cubic.toPoly {R : Type u_1} [] (P : ) :

Convert a cubic polynomial to a polynomial.

Instances For
theorem Cubic.C_mul_prod_X_sub_C_eq {S : Type u_2} [] {w : S} {x : S} {y : S} {z : S} :
Polynomial.C w * (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z) = Cubic.toPoly { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }
theorem Cubic.prod_X_sub_C_eq {S : Type u_2} [] {x : S} {y : S} {z : S} :
(Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z) = Cubic.toPoly { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }

### Coefficients #

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

### Degrees #

@[simp]
theorem Cubic.equiv_symm_apply_d {R : Type u_1} [] (f : { p // }) :
(Cubic.equiv.symm f).d = Polynomial.coeff (f) 0
@[simp]
theorem Cubic.equiv_symm_apply_b {R : Type u_1} [] (f : { p // }) :
(Cubic.equiv.symm f).b = Polynomial.coeff (f) 2
@[simp]
theorem Cubic.equiv_symm_apply_a {R : Type u_1} [] (f : { p // }) :
(Cubic.equiv.symm f).a = Polynomial.coeff (f) 3
@[simp]
theorem Cubic.equiv_symm_apply_c {R : Type u_1} [] (f : { p // }) :
(Cubic.equiv.symm f).c = Polynomial.coeff (f) 1
@[simp]
theorem Cubic.equiv_apply_coe {R : Type u_1} [] (P : ) :
↑(Cubic.equiv P) =
def Cubic.equiv {R : Type u_1} [] :
{ p // }

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

Instances For
@[simp]
theorem Cubic.degree_of_a_ne_zero {R : Type u_1} {P : } [] (ha : P.a 0) :
@[simp]
theorem Cubic.degree_of_a_ne_zero' {R : Type u_1} {a : R} {b : R} {c : R} {d : R} [] (ha : a 0) :
Polynomial.degree (Cubic.toPoly { a := a, b := b, c := c, d := d }) = 3
theorem Cubic.degree_of_a_eq_zero {R : Type u_1} {P : } [] (ha : P.a = 0) :
theorem Cubic.degree_of_a_eq_zero' {R : Type u_1} {b : R} {c : R} {d : R} [] :
Polynomial.degree (Cubic.toPoly { a := 0, b := b, c := c, d := d }) 2
@[simp]
theorem Cubic.degree_of_b_ne_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b 0) :
@[simp]
theorem Cubic.degree_of_b_ne_zero' {R : Type u_1} {b : R} {c : R} {d : R} [] (hb : b 0) :
Polynomial.degree (Cubic.toPoly { a := 0, b := b, c := c, d := d }) = 2
theorem Cubic.degree_of_b_eq_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b = 0) :
theorem Cubic.degree_of_b_eq_zero' {R : Type u_1} {c : R} {d : R} [] :
Polynomial.degree (Cubic.toPoly { a := 0, b := 0, c := c, d := d }) 1
@[simp]
theorem Cubic.degree_of_c_ne_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c 0) :
@[simp]
theorem Cubic.degree_of_c_ne_zero' {R : Type u_1} {c : R} {d : R} [] (hc : c 0) :
Polynomial.degree (Cubic.toPoly { a := 0, b := 0, c := c, d := d }) = 1
theorem Cubic.degree_of_c_eq_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :
theorem Cubic.degree_of_c_eq_zero' {R : Type u_1} {d : R} [] :
Polynomial.degree (Cubic.toPoly { a := 0, b := 0, c := 0, d := d }) 0
@[simp]
theorem Cubic.degree_of_d_ne_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d 0) :
@[simp]
theorem Cubic.degree_of_d_ne_zero' {R : Type u_1} {d : R} [] (hd : d 0) :
Polynomial.degree (Cubic.toPoly { a := 0, b := 0, c := 0, d := d }) = 0
@[simp]
theorem Cubic.degree_of_d_eq_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) :
theorem Cubic.degree_of_d_eq_zero' {R : Type u_1} [] :
Polynomial.degree (Cubic.toPoly { a := 0, b := 0, c := 0, d := 0 }) =
@[simp]
theorem Cubic.degree_of_zero {R : Type u_1} [] :
@[simp]
theorem Cubic.natDegree_of_a_ne_zero {R : Type u_1} {P : } [] (ha : P.a 0) :
@[simp]
theorem Cubic.natDegree_of_a_ne_zero' {R : Type u_1} {a : R} {b : R} {c : R} {d : R} [] (ha : a 0) :
Polynomial.natDegree (Cubic.toPoly { a := a, b := b, c := c, d := d }) = 3
theorem Cubic.natDegree_of_a_eq_zero {R : Type u_1} {P : } [] (ha : P.a = 0) :
theorem Cubic.natDegree_of_a_eq_zero' {R : Type u_1} {b : R} {c : R} {d : R} [] :
Polynomial.natDegree (Cubic.toPoly { a := 0, b := b, c := c, d := d }) 2
@[simp]
theorem Cubic.natDegree_of_b_ne_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b 0) :
@[simp]
theorem Cubic.natDegree_of_b_ne_zero' {R : Type u_1} {b : R} {c : R} {d : R} [] (hb : b 0) :
Polynomial.natDegree (Cubic.toPoly { a := 0, b := b, c := c, d := d }) = 2
theorem Cubic.natDegree_of_b_eq_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b = 0) :
theorem Cubic.natDegree_of_b_eq_zero' {R : Type u_1} {c : R} {d : R} [] :
Polynomial.natDegree (Cubic.toPoly { a := 0, b := 0, c := c, d := d }) 1
@[simp]
theorem Cubic.natDegree_of_c_ne_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c 0) :
@[simp]
theorem Cubic.natDegree_of_c_ne_zero' {R : Type u_1} {c : R} {d : R} [] (hc : c 0) :
Polynomial.natDegree (Cubic.toPoly { a := 0, b := 0, c := c, d := d }) = 1
@[simp]
theorem Cubic.natDegree_of_c_eq_zero {R : Type u_1} {P : } [] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :
theorem Cubic.natDegree_of_c_eq_zero' {R : Type u_1} {d : R} [] :
Polynomial.natDegree (Cubic.toPoly { a := 0, b := 0, c := 0, d := d }) = 0
@[simp]
theorem Cubic.natDegree_of_zero {R : Type u_1} [] :

### Map across a homomorphism #

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

Map a cubic polynomial across a semiring homomorphism.

Instances For
theorem Cubic.map_toPoly {R : Type u_1} {S : Type u_2} {P : } [] [] {φ : R →+* S} :

### Roots over an extension #

def Cubic.roots {R : Type u_1} [] [] (P : ) :

The roots of a cubic polynomial.

Instances For
theorem Cubic.map_roots {R : Type u_1} {S : Type u_2} {P : } [] [] {φ : R →+* S} [] :
theorem Cubic.mem_roots_iff {R : Type u_1} {P : } [] [] (h0 : ) (x : R) :
x P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
theorem Cubic.card_roots_le {R : Type u_1} {P : } [] [] [] :

### Roots over a splitting field #

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

### Discriminant over a splitting field #

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

The discriminant of a cubic polynomial.

Instances For
theorem Cubic.disc_eq_prod_three_roots {F : Type u_3} {K : Type u_4} {P : } [] [] {φ : F →+* K} {x : K} {y : K} {z : K} (ha : P.a 0) (h3 : Cubic.roots () = {x, y, z}) :
φ () = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
theorem Cubic.disc_ne_zero_iff_roots_ne {F : Type u_3} {K : Type u_4} {P : } [] [] {φ : F →+* K} {x : K} {y : K} {z : K} (ha : P.a 0) (h3 : Cubic.roots () = {x, y, z}) :
0 x y x z y z
theorem Cubic.disc_ne_zero_iff_roots_nodup {F : Type u_3} {K : Type u_4} {P : } [] [] {φ : F →+* K} {x : K} {y : K} {z : K} (ha : P.a 0) (h3 : Cubic.roots () = {x, y, z}) :
theorem Cubic.card_roots_of_disc_ne_zero {F : Type u_3} {K : Type u_4} {P : } [] [] {φ : F →+* K} {x : K} {y : K} {z : K} [] (ha : P.a 0) (h3 : Cubic.roots () = {x, y, z}) (hd : 0) :