Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-05 19:40 0f9c1538

View on Github →

feat(algebra/cubic_discriminant): basics of cubic polynomials and their discriminants (#11483)

Estimated changes

added theorem cubic.a_of_eq
added theorem cubic.b_eq_three_roots
added theorem cubic.b_of_eq
added theorem cubic.c_eq_three_roots
added theorem cubic.c_of_eq
added theorem cubic.card_roots_le
added theorem cubic.coeff_gt_three
added theorem cubic.coeff_one
added theorem cubic.coeff_three
added theorem cubic.coeff_two
added theorem cubic.coeff_zero
added theorem cubic.d_eq_three_roots
added theorem cubic.d_of_eq
added theorem cubic.degree
added theorem cubic.degree_of_zero
added def cubic.disc
added theorem cubic.eq_zero_iff
added def cubic.equiv
added theorem cubic.leading_coeff
added def cubic.map
added theorem cubic.map_roots
added theorem cubic.map_to_poly
added theorem cubic.mem_roots_iff
added theorem cubic.ne_zero
added theorem cubic.of_a_b_c_eq_zero
added theorem cubic.of_a_b_eq_zero
added theorem cubic.of_a_eq_zero
added theorem cubic.of_zero
added def cubic.roots
added def cubic.to_poly
added theorem cubic.zero
added structure cubic
modified theorem polynomial.coeff_C_mul_X
modified theorem polynomial.degree_C_lt