# mathlib3documentation

algebra.cubic_discriminant

# Cubics and discriminants #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

## Tags #

cubic, discriminant, polynomial, root

@[ext]
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 cubic
theorem cubic.ext {R : Type u_1} (x y : cubic R) (h : x.a = y.a) (h_1 : x.b = y.b) (h_2 : x.c = y.c) (h_3 : x.d = y.d) :
x = y
theorem cubic.ext_iff {R : Type u_1} (x y : cubic R) :
x = y x.a = y.a x.b = y.b x.c = y.c x.d = y.d
@[protected, instance]
def cubic.inhabited {R : Type u_1} [inhabited R] :
Equations
@[protected, instance]
def cubic.has_zero {R : Type u_1} [has_zero R] :
Equations
noncomputable def cubic.to_poly {R : Type u_1} [semiring R] (P : cubic R) :

Convert a cubic polynomial to a polynomial.

Equations
theorem cubic.C_mul_prod_X_sub_C_eq {S : Type u_2} [comm_ring S] {w x y z : S} :
* = {a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z)}.to_poly
theorem cubic.prod_X_sub_C_eq {S : Type u_2} [comm_ring S] {x y z : S} :
* = {a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z)}.to_poly

### Coefficients #

@[simp]
theorem cubic.coeff_eq_zero {R : Type u_1} {P : cubic R} [semiring R] {n : } (hn : 3 < n) :
@[simp]
theorem cubic.coeff_eq_a {R : Type u_1} {P : cubic R} [semiring R] :
@[simp]
theorem cubic.coeff_eq_b {R : Type u_1} {P : cubic R} [semiring R] :
@[simp]
theorem cubic.coeff_eq_c {R : Type u_1} {P : cubic R} [semiring R] :
@[simp]
theorem cubic.coeff_eq_d {R : Type u_1} {P : cubic R} [semiring R] :
theorem cubic.a_of_eq {R : Type u_1} {P Q : cubic R} [semiring R] (h : P.to_poly = Q.to_poly) :
P.a = Q.a
theorem cubic.b_of_eq {R : Type u_1} {P Q : cubic R} [semiring R] (h : P.to_poly = Q.to_poly) :
P.b = Q.b
theorem cubic.c_of_eq {R : Type u_1} {P Q : cubic R} [semiring R] (h : P.to_poly = Q.to_poly) :
P.c = Q.c
theorem cubic.d_of_eq {R : Type u_1} {P Q : cubic R} [semiring R] (h : P.to_poly = Q.to_poly) :
P.d = Q.d
theorem cubic.to_poly_injective {R : Type u_1} [semiring R] (P Q : cubic R) :
theorem cubic.of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) :
theorem cubic.of_a_eq_zero' {R : Type u_1} {b c d : R} [semiring R] :
{a := 0, b := b, c := c, d := d}.to_poly =
theorem cubic.of_b_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b = 0) :
theorem cubic.of_b_eq_zero' {R : Type u_1} {c d : R} [semiring R] :
{a := 0, b := 0, c := c, d := d}.to_poly =
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) :
theorem cubic.of_c_eq_zero' {R : Type u_1} {d : R} [semiring R] :
{a := 0, b := 0, c := 0, d := d}.to_poly =
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) :
theorem cubic.of_d_eq_zero' {R : Type u_1} [semiring R] :
{a := 0, b := 0, c := 0, d := 0}.to_poly = 0
theorem cubic.zero {R : Type u_1} [semiring R] :
theorem cubic.to_poly_eq_zero_iff {R : Type u_1} [semiring R] (P : cubic R) :
P.to_poly = 0 P = 0
theorem cubic.ne_zero_of_a_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a 0) :
theorem cubic.ne_zero_of_b_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (hb : P.b 0) :
theorem cubic.ne_zero_of_c_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (hc : P.c 0) :
theorem cubic.ne_zero_of_d_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (hd : P.d 0) :
@[simp]
theorem cubic.leading_coeff_of_a_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a 0) :
@[simp]
theorem cubic.leading_coeff_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}.to_poly.leading_coeff = a
@[simp]
theorem cubic.leading_coeff_of_b_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b 0) :
@[simp]
theorem cubic.leading_coeff_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}.to_poly.leading_coeff = b
@[simp]
theorem cubic.leading_coeff_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) :
@[simp]
theorem cubic.leading_coeff_of_c_ne_zero' {R : Type u_1} {c d : R} [semiring R] (hc : c 0) :
{a := 0, b := 0, c := c, d := d}.to_poly.leading_coeff = c
@[simp]
theorem cubic.leading_coeff_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) :
@[simp]
theorem cubic.leading_coeff_of_c_eq_zero' {R : Type u_1} {d : R} [semiring R] :
{a := 0, b := 0, c := 0, d := d}.to_poly.leading_coeff = d
theorem cubic.monic_of_a_eq_one {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 1) :
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}.to_poly.monic
theorem cubic.monic_of_b_eq_one {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b = 1) :
theorem cubic.monic_of_b_eq_one' {R : Type u_1} {c d : R} [semiring R] :
{a := 0, b := 1, c := c, d := d}.to_poly.monic
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) :
theorem cubic.monic_of_c_eq_one' {R : Type u_1} {d : R} [semiring R] :
{a := 0, b := 0, c := 1, d := d}.to_poly.monic
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) :
theorem cubic.monic_of_d_eq_one'  :
{a := 0, b := 0, c := 0, d := 1}.to_poly.monic

### Degrees #

@[simp]
theorem cubic.equiv_symm_apply_c {R : Type u_1} [semiring R] (f : {p // p.degree 3}) :
noncomputable def cubic.equiv {R : Type u_1} [semiring R] :
{p // p.degree 3}

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

Equations
@[simp]
theorem cubic.equiv_symm_apply_d {R : Type u_1} [semiring R] (f : {p // p.degree 3}) :
@[simp]
theorem cubic.equiv_symm_apply_b {R : Type u_1} [semiring R] (f : {p // p.degree 3}) :
@[simp]
theorem cubic.equiv_symm_apply_a {R : Type u_1} [semiring R] (f : {p // p.degree 3}) :
@[simp]
theorem cubic.equiv_apply_coe {R : Type u_1} [semiring R] (P : cubic R) :
@[simp]
theorem cubic.degree_of_a_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a 0) :
@[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}.to_poly.degree = 3
theorem cubic.degree_of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) :
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}.to_poly.degree 2
@[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) :
@[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}.to_poly.degree = 2
theorem cubic.degree_of_b_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b = 0) :
theorem cubic.degree_of_b_eq_zero' {R : Type u_1} {c d : R} [semiring R] :
{a := 0, b := 0, c := c, d := d}.to_poly.degree 1
@[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) :
@[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}.to_poly.degree = 1
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) :
theorem cubic.degree_of_c_eq_zero' {R : Type u_1} {d : R} [semiring R] :
{a := 0, b := 0, c := 0, d := d}.to_poly.degree 0
@[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) :
@[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}.to_poly.degree = 0
@[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) :
@[simp]
theorem cubic.degree_of_d_eq_zero' {R : Type u_1} [semiring R] :
{a := 0, b := 0, c := 0, d := 0}.to_poly.degree =
@[simp]
theorem cubic.degree_of_zero {R : Type u_1} [semiring R] :
@[simp]
theorem cubic.nat_degree_of_a_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a 0) :
@[simp]
theorem cubic.nat_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}.to_poly.nat_degree = 3
theorem cubic.nat_degree_of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) :
theorem cubic.nat_degree_of_a_eq_zero' {R : Type u_1} {b c d : R} [semiring R] :
{a := 0, b := b, c := c, d := d}.to_poly.nat_degree 2
@[simp]
theorem cubic.nat_degree_of_b_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b 0) :
@[simp]
theorem cubic.nat_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}.to_poly.nat_degree = 2
theorem cubic.nat_degree_of_b_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b = 0) :
theorem cubic.nat_degree_of_b_eq_zero' {R : Type u_1} {c d : R} [semiring R] :
{a := 0, b := 0, c := c, d := d}.to_poly.nat_degree 1
@[simp]
theorem cubic.nat_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) :
@[simp]
theorem cubic.nat_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}.to_poly.nat_degree = 1
@[simp]
theorem cubic.nat_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) :
@[simp]
theorem cubic.nat_degree_of_c_eq_zero' {R : Type u_1} {d : R} [semiring R] :
{a := 0, b := 0, c := 0, d := d}.to_poly.nat_degree = 0
@[simp]
theorem cubic.nat_degree_of_zero {R : Type u_1} [semiring R] :

### Map across a homomorphism #

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

Map a cubic polynomial across a semiring homomorphism.

Equations
theorem cubic.map_to_poly {R : Type u_1} {S : Type u_2} {P : cubic R} [semiring R] [semiring S] {φ : R →+* S} :
P).to_poly =

### Roots over an extension #

noncomputable def cubic.roots {R : Type u_1} [comm_ring R] [is_domain R] (P : cubic R) :

The roots of a cubic polynomial.

Equations
theorem cubic.map_roots {R : Type u_1} {S : Type u_2} {P : cubic R} [comm_ring R] [comm_ring S] {φ : R →+* S} [is_domain S] :
theorem cubic.mem_roots_iff {R : Type u_1} {P : cubic R} [comm_ring R] [is_domain R] (h0 : P.to_poly 0) (x : R) :
x P.roots P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
theorem cubic.card_roots_le {R : Type u_1} {P : cubic R} [comm_ring R] [is_domain R] [decidable_eq R] :

### Roots over a splitting field #

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) :
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) :
(x y z : K), P).roots = {x, y, z}
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 : P).roots = {x, y, z}) :
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 : P).roots = {x, y, z}) :
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)}
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 : P).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 : cubic F} [field F] [field K] {φ : F →+* K} {x y z : K} (ha : P.a 0) (h3 : P).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 : cubic F} [field F] [field K] {φ : F →+* K} {x y z : K} (ha : P.a 0) (h3 : P).roots = {x, y, z}) :
φ P.d = φ P.a * -(x * y * z)

### Discriminant over a splitting field #

def cubic.disc {R : Type u_1} [ring R] (P : cubic R) :
R

The discriminant of a cubic polynomial.

Equations
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 : P).roots = {x, y, z}) :
φ P.disc = (φ 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 : cubic F} [field F] [field K] {φ : F →+* K} {x y z : K} (ha : P.a 0) (h3 : P).roots = {x, y, z}) :
P.disc 0 x y x z y z
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 : P).roots = {x, y, z}) :
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} [decidable_eq K] (ha : P.a 0) (h3 : P).roots = {x, y, z}) (hd : P.disc 0) :