Mathlib Changelog
Changelog
About
Github
Commit
2022-02-05 19:40
0f9c1538
View on Github →
feat(algebra/cubic_discriminant): basics of cubic polynomials and their discriminants (
#11483
)
Estimated changes
Created
src/algebra/cubic_discriminant.lean
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.card_roots_of_disc_ne_zero
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_a_b_c_eq_zero
added
theorem
cubic.degree_of_a_b_eq_zero
added
theorem
cubic.degree_of_a_eq_zero
added
theorem
cubic.degree_of_zero
added
def
cubic.disc
added
theorem
cubic.disc_eq_prod_three_roots
added
theorem
cubic.disc_ne_zero_iff_roots_ne
added
theorem
cubic.disc_ne_zero_iff_roots_nodup
added
theorem
cubic.eq_prod_three_roots
added
theorem
cubic.eq_sum_three_roots
added
theorem
cubic.eq_zero_iff
added
def
cubic.equiv
added
theorem
cubic.leading_coeff
added
theorem
cubic.leading_coeff_of_a_b_c_eq_zero
added
theorem
cubic.leading_coeff_of_a_b_eq_zero
added
theorem
cubic.leading_coeff_of_a_eq_zero
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.ne_zero_of_a_ne_zero
added
theorem
cubic.ne_zero_of_b_ne_zero
added
theorem
cubic.ne_zero_of_c_ne_zero
added
theorem
cubic.ne_zero_of_d_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
theorem
cubic.splits_iff_card_roots
added
theorem
cubic.splits_iff_roots_eq_three
added
def
cubic.to_poly
added
theorem
cubic.to_poly_injective
added
theorem
cubic.zero
added
structure
cubic
Modified
src/data/polynomial/coeff.lean
modified
theorem
polynomial.coeff_C_mul_X
added
theorem
polynomial.coeff_C_mul_X_pow
Modified
src/data/polynomial/degree/definitions.lean
modified
theorem
polynomial.degree_C_lt
added
theorem
polynomial.degree_C_lt_degree_C_mul_X
added
theorem
polynomial.degree_C_mul_X
added
theorem
polynomial.degree_add_le_of_degree_le
added
theorem
polynomial.degree_cubic
added
theorem
polynomial.degree_cubic_le
added
theorem
polynomial.degree_cubic_lt
added
theorem
polynomial.degree_linear
added
theorem
polynomial.degree_linear_le
added
theorem
polynomial.degree_linear_lt
added
theorem
polynomial.degree_linear_lt_degree_C_mul_X_sq
added
theorem
polynomial.degree_quadratic
added
theorem
polynomial.degree_quadratic_le
added
theorem
polynomial.degree_quadratic_lt
added
theorem
polynomial.degree_quadratic_lt_degree_C_mul_X_cb
added
theorem
polynomial.leading_coeff_C_mul_X
deleted
theorem
polynomial.leading_coeff_C_mul_X_add_C
added
theorem
polynomial.leading_coeff_cubic
added
theorem
polynomial.leading_coeff_linear
added
theorem
polynomial.leading_coeff_quadratic
added
theorem
polynomial.nat_degree_add_le_of_degree_le
added
theorem
polynomial.nat_degree_cubic
added
theorem
polynomial.nat_degree_cubic_le
added
theorem
polynomial.nat_degree_linear
added
theorem
polynomial.nat_degree_linear_le
added
theorem
polynomial.nat_degree_quadratic
added
theorem
polynomial.nat_degree_quadratic_le
Modified
src/data/polynomial/eval.lean
Modified
src/ring_theory/polynomial/vieta.lean
Modified
src/ring_theory/power_series/basic.lean
deleted
theorem
power_series.coeff_C_mul_X
added
theorem
power_series.coeff_C_mul_X_pow