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.
References #
Tags #
cubic, discriminant, polynomial, root
@[ext]
- a : R
- b : R
- c : R
- d : R
The structure representing a cubic polynomial.
Instances for cubic
- cubic.has_sizeof_inst
- cubic.inhabited
- cubic.has_zero
@[protected, instance]
Equations
- cubic.inhabited = {default := {a := inhabited.default _inst_1, b := inhabited.default _inst_1, c := inhabited.default _inst_1, d := inhabited.default _inst_1}}
Convert a cubic polynomial to a polynomial.
Equations
- P.to_poly = ⇑polynomial.C P.a * polynomial.X ^ 3 + ⇑polynomial.C P.b * polynomial.X ^ 2 + ⇑polynomial.C P.c * polynomial.X + ⇑polynomial.C P.d
Coefficients #
@[simp]
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
@[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) :
P.to_poly = ⇑polynomial.C P.c * polynomial.X + ⇑polynomial.C P.d
Degrees #
The equivalence between cubic polynomials and polynomials of degree at most three.
@[simp]
theorem
cubic.equiv_apply_coe
{R : Type u_1}
[semiring R]
(P : cubic R) :
↑(⇑cubic.equiv P) = P.to_poly
theorem
cubic.leading_coeff
{R : Type u_1}
{P : cubic R}
[semiring R]
(ha : P.a ≠ 0) :
P.to_poly.leading_coeff = P.a
Map across a homomorphism #
Roots over an extension #
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.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)