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 : Cubic R) (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

theorem Cubic.ext_iff {R : Type u_1} (x : Cubic R) (y : Cubic R) : 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

The structure representing a cubic polynomial.

• a : R
• b : R
• c : R
• d : R

instance Cubic.instInhabitedCubic {R : Type u_1} [Inhabited R] : Inhabited (Cubic R)

Equations

• Cubic.instInhabitedCubic = { default := { a := default, b := default, c := default, d := default } }

instance Cubic.instZeroCubic {R : Type u_1} [Zero R] : Zero (Cubic R)

Equations

• Cubic.instZeroCubic = { zero := { a := 0, b := 0, c := 0, d := 0 } }

def Cubic.toPoly {R : Type u_1} [Semiring R] (P : Cubic R) : Polynomial R

Convert a cubic polynomial to a polynomial.

Equations

• Cubic.toPoly P = Polynomial.C P.a * Polynomial.X ^ 3 + Polynomial.C P.b * Polynomial.X ^ 2 + Polynomial.C P.c * Polynomial.X + Polynomial.C P.d

theorem Cubic.C_mul_prod_X_sub_C_eq {S : Type u_2} [CommRing S] {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} [CommRing S] {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 : Cubic R} [Semiring R] {n : ℕ} (hn : 3 < n) : Polynomial.coeff (Cubic.toPoly P) n = 0

@[simp]

theorem Cubic.coeff_eq_a {R : Type u_1} {P : Cubic R} [Semiring R] : Polynomial.coeff (Cubic.toPoly P) 3 = P.a

@[simp]

theorem Cubic.coeff_eq_b {R : Type u_1} {P : Cubic R} [Semiring R] : Polynomial.coeff (Cubic.toPoly P) 2 = P.b

@[simp]

theorem Cubic.coeff_eq_c {R : Type u_1} {P : Cubic R} [Semiring R] : Polynomial.coeff (Cubic.toPoly P) 1 = P.c

@[simp]

theorem Cubic.coeff_eq_d {R : Type u_1} {P : Cubic R} [Semiring R] : Polynomial.coeff (Cubic.toPoly P) 0 = P.d

theorem Cubic.a_of_eq {R : Type u_1} {P : Cubic R} {Q : Cubic R} [Semiring R] (h : Cubic.toPoly P = Cubic.toPoly Q) : P.a = Q.a

theorem Cubic.b_of_eq {R : Type u_1} {P : Cubic R} {Q : Cubic R} [Semiring R] (h : Cubic.toPoly P = Cubic.toPoly Q) : P.b = Q.b

theorem Cubic.c_of_eq {R : Type u_1} {P : Cubic R} {Q : Cubic R} [Semiring R] (h : Cubic.toPoly P = Cubic.toPoly Q) : P.c = Q.c

theorem Cubic.d_of_eq {R : Type u_1} {P : Cubic R} {Q : Cubic R} [Semiring R] (h : Cubic.toPoly P = Cubic.toPoly Q) : P.d = Q.d

theorem Cubic.toPoly_injective {R : Type u_1} [Semiring R] (P : Cubic R) (Q : Cubic R) : Cubic.toPoly P = Cubic.toPoly Q ↔ P = Q

theorem Cubic.of_a_eq_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) : Cubic.toPoly P = 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} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) : Cubic.toPoly P = Polynomial.C P.c * Polynomial.X + Polynomial.C P.d

theorem Cubic.of_b_eq_zero' {R : Type u_1} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : Cubic.toPoly P = Polynomial.C P.d

theorem Cubic.of_c_eq_zero' {R : Type u_1} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) : Cubic.toPoly P = 0

theorem Cubic.of_d_eq_zero' {R : Type u_1} [Semiring R] : Cubic.toPoly { a := 0, b := 0, c := 0, d := 0 } = 0

theorem Cubic.zero {R : Type u_1} [Semiring R] : Cubic.toPoly 0 = 0

theorem Cubic.toPoly_eq_zero_iff {R : Type u_1} [Semiring R] (P : Cubic R) : Cubic.toPoly P = 0 ↔ P = 0

theorem Cubic.ne_zero_of_a_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) : Cubic.toPoly P ≠ 0

theorem Cubic.ne_zero_of_b_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (hb : P.b ≠ 0) : Cubic.toPoly P ≠ 0

theorem Cubic.ne_zero_of_c_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (hc : P.c ≠ 0) : Cubic.toPoly P ≠ 0

theorem Cubic.ne_zero_of_d_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (hd : P.d ≠ 0) : Cubic.toPoly P ≠ 0

@[simp]

theorem Cubic.leadingCoeff_of_a_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) : Polynomial.leadingCoeff (Cubic.toPoly P) = P.a

@[simp]

theorem Cubic.leadingCoeff_of_a_ne_zero' {R : Type u_1} {a : R} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b ≠ 0) : Polynomial.leadingCoeff (Cubic.toPoly P) = P.b

@[simp]

theorem Cubic.leadingCoeff_of_b_ne_zero' {R : Type u_1} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : Polynomial.leadingCoeff (Cubic.toPoly P) = P.c

@[simp]

theorem Cubic.leadingCoeff_of_c_ne_zero' {R : Type u_1} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : Polynomial.leadingCoeff (Cubic.toPoly P) = P.d

theorem Cubic.leadingCoeff_of_c_eq_zero' {R : Type u_1} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 1) : Polynomial.Monic (Cubic.toPoly P)

theorem Cubic.monic_of_a_eq_one' {R : Type u_1} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 1) : Polynomial.Monic (Cubic.toPoly P)

theorem Cubic.monic_of_b_eq_one' {R : Type u_1} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 1) : Polynomial.Monic (Cubic.toPoly P)

theorem Cubic.monic_of_c_eq_one' {R : Type u_1} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 1) : Polynomial.Monic (Cubic.toPoly P)

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} [Semiring R] (f : { p : Polynomial R // Polynomial.degree p ≤ 3 }) : (Cubic.equiv.symm f).d = Polynomial.coeff (↑f) 0

@[simp]

theorem Cubic.equiv_symm_apply_b {R : Type u_1} [Semiring R] (f : { p : Polynomial R // Polynomial.degree p ≤ 3 }) : (Cubic.equiv.symm f).b = Polynomial.coeff (↑f) 2

@[simp]

theorem Cubic.equiv_symm_apply_a {R : Type u_1} [Semiring R] (f : { p : Polynomial R // Polynomial.degree p ≤ 3 }) : (Cubic.equiv.symm f).a = Polynomial.coeff (↑f) 3

@[simp]

theorem Cubic.equiv_symm_apply_c {R : Type u_1} [Semiring R] (f : { p : Polynomial R // Polynomial.degree p ≤ 3 }) : (Cubic.equiv.symm f).c = Polynomial.coeff (↑f) 1

@[simp]

theorem Cubic.equiv_apply_coe {R : Type u_1} [Semiring R] (P : Cubic R) : ↑(Cubic.equiv P) = Cubic.toPoly P

def Cubic.equiv {R : Type u_1} [Semiring R] : Cubic R ≃ { p : Polynomial R // Polynomial.degree p ≤ 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.

@[simp]

theorem Cubic.degree_of_a_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) : Polynomial.degree (Cubic.toPoly P) = 3

@[simp]

theorem Cubic.degree_of_a_ne_zero' {R : Type u_1} {a : R} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) : Polynomial.degree (Cubic.toPoly P) ≤ 2

theorem Cubic.degree_of_a_eq_zero' {R : Type u_1} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b ≠ 0) : Polynomial.degree (Cubic.toPoly P) = 2

@[simp]

theorem Cubic.degree_of_b_ne_zero' {R : Type u_1} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) : Polynomial.degree (Cubic.toPoly P) ≤ 1

theorem Cubic.degree_of_b_eq_zero' {R : Type u_1} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : Polynomial.degree (Cubic.toPoly P) = 1

@[simp]

theorem Cubic.degree_of_c_ne_zero' {R : Type u_1} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : Polynomial.degree (Cubic.toPoly P) ≤ 0

theorem Cubic.degree_of_c_eq_zero' {R : Type u_1} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d ≠ 0) : Polynomial.degree (Cubic.toPoly P) = 0

@[simp]

theorem Cubic.degree_of_d_ne_zero' {R : Type u_1} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) : Polynomial.degree (Cubic.toPoly P) = ⊥

theorem Cubic.degree_of_d_eq_zero' {R : Type u_1} [Semiring R] : Polynomial.degree (Cubic.toPoly { a := 0, b := 0, c := 0, d := 0 }) = ⊥

@[simp]

theorem Cubic.degree_of_zero {R : Type u_1} [Semiring R] : Polynomial.degree (Cubic.toPoly 0) = ⊥

@[simp]

theorem Cubic.natDegree_of_a_ne_zero {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) : Polynomial.natDegree (Cubic.toPoly P) = 3

@[simp]

theorem Cubic.natDegree_of_a_ne_zero' {R : Type u_1} {a : R} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) : Polynomial.natDegree (Cubic.toPoly P) ≤ 2

theorem Cubic.natDegree_of_a_eq_zero' {R : Type u_1} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b ≠ 0) : Polynomial.natDegree (Cubic.toPoly P) = 2

@[simp]

theorem Cubic.natDegree_of_b_ne_zero' {R : Type u_1} {b : R} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) : Polynomial.natDegree (Cubic.toPoly P) ≤ 1

theorem Cubic.natDegree_of_b_eq_zero' {R : Type u_1} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : Polynomial.natDegree (Cubic.toPoly P) = 1

@[simp]

theorem Cubic.natDegree_of_c_ne_zero' {R : Type u_1} {c : R} {d : R} [Semiring 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 : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : Polynomial.natDegree (Cubic.toPoly P) = 0

theorem Cubic.natDegree_of_c_eq_zero' {R : Type u_1} {d : R} [Semiring R] : Polynomial.natDegree (Cubic.toPoly { a := 0, b := 0, c := 0, d := d }) = 0

@[simp]

theorem Cubic.natDegree_of_zero {R : Type u_1} [Semiring R] : Polynomial.natDegree (Cubic.toPoly 0) = 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) : 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 }

theorem Cubic.map_toPoly {R : Type u_1} {S : Type u_2} {P : Cubic R} [Semiring R] [Semiring S] {φ : R →+* S} : Cubic.toPoly (Cubic.map φ P) = Polynomial.map φ (Cubic.toPoly P)

Roots over an extension

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

The roots of a cubic polynomial.

Equations

• Cubic.roots P = Polynomial.roots (Cubic.toPoly P)

theorem Cubic.map_roots {R : Type u_1} {S : Type u_2} {P : Cubic R} [CommRing R] [CommRing S] {φ : R →+* S} [IsDomain S] : Cubic.roots (Cubic.map φ P) = Polynomial.roots (Polynomial.map φ (Cubic.toPoly P))

theorem Cubic.mem_roots_iff {R : Type u_1} {P : Cubic R} [CommRing R] [IsDomain R] (h0 : Cubic.toPoly P ≠ 0) (x : R) : x ∈ Cubic.roots P ↔ 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} [CommRing R] [IsDomain R] [DecidableEq R] : (Multiset.toFinset (Cubic.roots P)).card ≤ 3

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) : Polynomial.Splits φ (Cubic.toPoly P) ↔ Multiset.card (Cubic.roots (Cubic.map φ P)) = 3

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 φ (Cubic.toPoly P) ↔ ∃ (x : K) (y : K) (z : K), Cubic.roots (Cubic.map φ P) = {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 : K} {y : K} {z : K} (ha : P.a ≠ 0) (h3 : Cubic.roots (Cubic.map φ P) = {x, y, z}) : Cubic.toPoly (Cubic.map φ P) = 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 : Cubic F} [Field F] [Field K] {φ : F →+* K} {x : K} {y : K} {z : K} (ha : P.a ≠ 0) (h3 : Cubic.roots (Cubic.map φ P) = {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) }

theorem Cubic.b_eq_three_roots {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x : K} {y : K} {z : K} (ha : P.a ≠ 0) (h3 : Cubic.roots (Cubic.map φ P) = {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 : K} {y : K} {z : K} (ha : P.a ≠ 0) (h3 : Cubic.roots (Cubic.map φ P) = {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 : K} {y : K} {z : K} (ha : P.a ≠ 0) (h3 : Cubic.roots (Cubic.map φ P) = {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 : Cubic R) : R

The discriminant of a cubic polynomial.

Equations

• Cubic.disc P = 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

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 : K} {y : K} {z : K} (ha : P.a ≠ 0) (h3 : Cubic.roots (Cubic.map φ P) = {x, y, z}) : φ (Cubic.disc P) = (φ 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 : K} {y : K} {z : K} (ha : P.a ≠ 0) (h3 : Cubic.roots (Cubic.map φ P) = {x, y, z}) : Cubic.disc P ≠ 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 : K} {y : K} {z : K} (ha : P.a ≠ 0) (h3 : Cubic.roots (Cubic.map φ P) = {x, y, z}) : Cubic.disc P ≠ 0 ↔ Multiset.Nodup (Cubic.roots (Cubic.map φ P))

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