mathlib3 documentation

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 #

Main statements #

References #

Tags #

cubic, discriminant, polynomial, root

source
@[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
source
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
source
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
source
@[protected, instance]
def cubic.inhabited {R : Type u_1} [inhabited R] :
inhabited (cubic R)
Equations
source
@[protected, instance]
def cubic.has_zero {R : Type u_1} [has_zero R] :
has_zero (cubic R)
Equations
source
noncomputable def cubic.to_poly {R : Type u_1} [semiring R] (P : cubic R) :
polynomial R

Convert a cubic polynomial to a polynomial.

Equations
source
theorem cubic.C_mul_prod_X_sub_C_eq {S : Type u_2} [comm_ring 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)}.to_poly
source
theorem cubic.prod_X_sub_C_eq {S : Type u_2} [comm_ring 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)}.to_poly

Coefficients #

source
@[simp]
theorem cubic.coeff_eq_zero {R : Type u_1} {P : cubic R} [semiring R] {n : ℕ} (hn : 3 < n) :
P.to_poly.coeff n = 0
source
@[simp]
theorem cubic.coeff_eq_a {R : Type u_1} {P : cubic R} [semiring R] :
P.to_poly.coeff 3 = P.a
source
@[simp]
theorem cubic.coeff_eq_b {R : Type u_1} {P : cubic R} [semiring R] :
P.to_poly.coeff 2 = P.b
source
@[simp]
theorem cubic.coeff_eq_c {R : Type u_1} {P : cubic R} [semiring R] :
P.to_poly.coeff 1 = P.c
source
@[simp]
theorem cubic.coeff_eq_d {R : Type u_1} {P : cubic R} [semiring R] :
P.to_poly.coeff 0 = P.d
source
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
source
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
source
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
source
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
source
theorem cubic.to_poly_injective {R : Type u_1} [semiring R] (P Q : cubic R) :
P.to_poly = Q.to_poly ↔ P = Q
source
theorem cubic.of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) :
P.to_poly = ⇑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}.to_poly = ⇑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.to_poly = ⇑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}.to_poly = ⇑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.to_poly = ⇑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}.to_poly = ⇑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.to_poly = 0
source
theorem cubic.of_d_eq_zero' {R : Type u_1} [semiring R] :
{a := 0, b := 0, c := 0, d := 0}.to_poly = 0
source
theorem cubic.zero {R : Type u_1} [semiring R] :
0.to_poly = 0
source
theorem cubic.to_poly_eq_zero_iff {R : Type u_1} [semiring R] (P : cubic R) :
P.to_poly = 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.to_poly ≠ 0
source
theorem cubic.ne_zero_of_b_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (hb : P.b ≠ 0) :
P.to_poly ≠ 0
source
theorem cubic.ne_zero_of_c_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (hc : P.c ≠ 0) :
P.to_poly ≠ 0
source
theorem cubic.ne_zero_of_d_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (hd : P.d ≠ 0) :
P.to_poly ≠ 0
source
@[simp]
theorem cubic.leading_coeff_of_a_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a ≠ 0) :
P.to_poly.leading_coeff = P.a
source
@[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
source
@[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) :
P.to_poly.leading_coeff = P.b
source
@[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
source
@[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) :
P.to_poly.leading_coeff = P.c
source
@[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
source
@[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) :
P.to_poly.leading_coeff = P.d
source
@[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
source
theorem cubic.monic_of_a_eq_one {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 1) :
P.to_poly.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}.to_poly.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.to_poly.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}.to_poly.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.to_poly.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}.to_poly.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.to_poly.monic
source
theorem cubic.monic_of_d_eq_one'  :
{a := 0, b := 0, c := 0, d := 1}.to_poly.monic

Degrees #

source
@[simp]
theorem cubic.equiv_symm_apply_c {R : Type u_1} [semiring R] (f : {p // p.degree ≤ 3}) :
(⇑(cubic.equiv.symm) f).c = ↑f.coeff 1
source
noncomputable def cubic.equiv {R : Type u_1} [semiring R] :
cubic R ≃ {p // p.degree ≤ 3}

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

Equations
source
@[simp]
theorem cubic.equiv_symm_apply_d {R : Type u_1} [semiring R] (f : {p // 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 // p.degree ≤ 3}) :
(⇑(cubic.equiv.symm) f).b = ↑f.coeff 2
source
@[simp]
theorem cubic.equiv_symm_apply_a {R : Type u_1} [semiring R] (f : {p // p.degree ≤ 3}) :
(⇑(cubic.equiv.symm) f).a = ↑f.coeff 3
source
@[simp]
theorem cubic.equiv_apply_coe {R : Type u_1} [semiring R] (P : cubic R) :
↑(⇑cubic.equiv P) = P.to_poly
source
@[simp]
theorem cubic.degree_of_a_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a ≠ 0) :
P.to_poly.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}.to_poly.degree = 3
source
theorem cubic.degree_of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) :
P.to_poly.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}.to_poly.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.to_poly.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}.to_poly.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.to_poly.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}.to_poly.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.to_poly.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}.to_poly.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.to_poly.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}.to_poly.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.to_poly.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}.to_poly.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.to_poly.degree = ⊥
source
@[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 = ⊥
source
@[simp]
theorem cubic.degree_of_zero {R : Type u_1} [semiring R] :
0.to_poly.degree = ⊥
source
@[simp]
theorem cubic.nat_degree_of_a_ne_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a ≠ 0) :
P.to_poly.nat_degree = 3
source
@[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
source
theorem cubic.nat_degree_of_a_eq_zero {R : Type u_1} {P : cubic R} [semiring R] (ha : P.a = 0) :
P.to_poly.nat_degree ≤ 2
source
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
source
@[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) :
P.to_poly.nat_degree = 2
source
@[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
source
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) :
P.to_poly.nat_degree ≤ 1
source
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
source
@[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) :
P.to_poly.nat_degree = 1
source
@[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
source
@[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) :
P.to_poly.nat_degree = 0
source
@[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
source
@[simp]
theorem cubic.nat_degree_of_zero {R : Type u_1} [semiring R] :
0.to_poly.nat_degree = 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
source
theorem cubic.map_to_poly {R : Type u_1} {S : Type u_2} {P : cubic R} [semiring R] [semiring S] {φ : R →+* S} :
(cubic.map φ P).to_poly = polynomial.map φ P.to_poly

Roots over an extension #

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

The roots of a cubic polynomial.

Equations
source
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] :
(cubic.map φ P).roots = (polynomial.map φ P.to_poly).roots
source
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
source
theorem cubic.card_roots_le {R : Type u_1} {P : cubic R} [comm_ring R] [is_domain R] [decidable_eq R] :
P.roots.to_finset.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.to_poly ↔ ⇑multiset.card (cubic.map φ P).roots = 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.to_poly ↔ ∃ (x y 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).to_poly = ⇑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_1} [ring R] (P : cubic R) :
R

The discriminant of a cubic polynomial.

Equations
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} [decidable_eq K] (ha : P.a ≠ 0) (h3 : (cubic.map φ P).roots = {x, y, z}) (hd : P.disc ≠ 0) :
(cubic.map φ P).roots.to_finset.card = 3