# mathlibdocumentation

algebra.cubic_discriminant

# 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.
• disc: the discriminant of a cubic polynomial.

## Main statements #

• 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

### Coefficients #

@[simp]
theorem cubic.coeff_gt_three {R : Type u_1} {P : cubic R} [semiring R] (n : ) (hn : 3 < n) :
@[simp]
theorem cubic.coeff_three {R : Type u_1} {P : cubic R} [semiring R] :
@[simp]
theorem cubic.coeff_two {R : Type u_1} {P : cubic R} [semiring R] :
@[simp]
theorem cubic.coeff_one {R : Type u_1} {P : cubic R} [semiring R] :
@[simp]
theorem cubic.coeff_zero {R : Type u_1} {P : cubic R} [semiring R] :
theorem cubic.a_of_eq {R : Type u_1} {P : cubic R} [semiring R] {Q : cubic R} (h : P.to_poly = Q.to_poly) :
P.a = Q.a
theorem cubic.b_of_eq {R : Type u_1} {P : cubic R} [semiring R] {Q : cubic R} (h : P.to_poly = Q.to_poly) :
P.b = Q.b
theorem cubic.c_of_eq {R : Type u_1} {P : cubic R} [semiring R] {Q : cubic R} (h : P.to_poly = Q.to_poly) :
P.c = Q.c
theorem cubic.d_of_eq {R : Type u_1} {P : cubic R} [semiring R] {Q : cubic R} (h : P.to_poly = Q.to_poly) :
P.d = Q.d
@[simp]
theorem cubic.to_poly_injective {R : Type u_1} [semiring R] (P Q : cubic R) :
@[simp]
theorem cubic.of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) :
@[simp]
theorem cubic.of_a_b_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b = 0) :
@[simp]
theorem cubic.of_a_b_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.of_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.zero {R : Type u_1} [semiring R] :
@[simp]
theorem cubic.eq_zero_iff {R : Type u_1} {P : cubic R} [semiring R] :
P.to_poly = 0 P = 0
theorem cubic.ne_zero {R : Type u_1} {P : cubic R} [semiring R] (h0 : ¬P.a = 0 ¬P.b = 0 ¬P.c = 0 ¬P.d = 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) :

### 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) :
theorem cubic.degree {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a 0) :
theorem cubic.degree_of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b 0) :
theorem cubic.degree_of_a_b_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_a_b_c_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.degree_of_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.leading_coeff {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a 0) :
theorem cubic.leading_coeff_of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b 0) :
theorem cubic.leading_coeff_of_a_b_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.leading_coeff_of_a_b_c_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :

### 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) :