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, discriminant, polynomial, root
The structure representing a cubic polynomial.
Convert a cubic polynomial to a polynomial.
The equivalence between cubic polynomials and polynomials of degree at most three.
Map across a homomorphism #
Map a cubic polynomial across a semiring homomorphism.
Roots over an extension #
The roots of a cubic polynomial.
Roots over a splitting field #
Discriminant over a splitting field #
The discriminant of a cubic polynomial.