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.
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.