Commit 2022-11-24 10:55 c1d80c11

View on Github →

feat(algebra/cubic_discriminant): add eq_zero and ne_zero lemmas (#17627) E.g. to allow degree_of_c_eq_zero' instead of degree_of_c_eq_zero rfl rfl rfl when the cubic is known to be constant.

Estimated changes

Modified src/algebra/cubic_discriminant.lean

modified theorem cubic.a_of_eq

modified theorem cubic.b_of_eq

modified theorem cubic.c_of_eq

added theorem cubic.coeff_eq_a

added theorem cubic.coeff_eq_b

added theorem cubic.coeff_eq_c

added theorem cubic.coeff_eq_d

added theorem cubic.coeff_eq_zero

deleted theorem cubic.coeff_gt_three

deleted theorem cubic.coeff_one

deleted theorem cubic.coeff_three

deleted theorem cubic.coeff_two

deleted theorem cubic.coeff_zero

modified theorem cubic.d_of_eq

deleted theorem cubic.degree

deleted theorem cubic.degree_of_a_b_c_eq_zero

deleted theorem cubic.degree_of_a_b_eq_zero

added theorem cubic.degree_of_a_eq_zero'

modified theorem cubic.degree_of_a_eq_zero

added theorem cubic.degree_of_a_ne_zero'

added theorem cubic.degree_of_a_ne_zero

added theorem cubic.degree_of_b_eq_zero'

added theorem cubic.degree_of_b_eq_zero

added theorem cubic.degree_of_b_ne_zero'

added theorem cubic.degree_of_b_ne_zero

added theorem cubic.degree_of_c_eq_zero'

added theorem cubic.degree_of_c_eq_zero

added theorem cubic.degree_of_c_ne_zero'

added theorem cubic.degree_of_c_ne_zero

added theorem cubic.degree_of_d_eq_zero'

added theorem cubic.degree_of_d_eq_zero

added theorem cubic.degree_of_d_ne_zero'

added theorem cubic.degree_of_d_ne_zero

modified theorem cubic.degree_of_zero

deleted theorem cubic.eq_zero_iff

deleted theorem cubic.leading_coeff

deleted theorem cubic.leading_coeff_of_a_b_c_eq_zero

deleted theorem cubic.leading_coeff_of_a_b_eq_zero

deleted theorem cubic.leading_coeff_of_a_eq_zero

added theorem cubic.leading_coeff_of_a_ne_zero'

added theorem cubic.leading_coeff_of_a_ne_zero

added theorem cubic.leading_coeff_of_b_ne_zero'

added theorem cubic.leading_coeff_of_b_ne_zero

added theorem cubic.leading_coeff_of_c_eq_zero'

added theorem cubic.leading_coeff_of_c_eq_zero

added theorem cubic.leading_coeff_of_c_ne_zero'

added theorem cubic.leading_coeff_of_c_ne_zero

deleted theorem cubic.ne_zero

deleted theorem cubic.of_a_b_c_eq_zero

deleted theorem cubic.of_a_b_eq_zero

added theorem cubic.of_a_eq_zero'

modified theorem cubic.of_a_eq_zero

added theorem cubic.of_b_eq_zero'

added theorem cubic.of_b_eq_zero

added theorem cubic.of_c_eq_zero'

added theorem cubic.of_c_eq_zero

added theorem cubic.of_d_eq_zero'

added theorem cubic.of_d_eq_zero

deleted theorem cubic.of_zero

added theorem cubic.to_poly_eq_zero_iff

modified theorem cubic.to_poly_injective

modified theorem cubic.zero