Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 19:45 6f11155d

View on Github →

feat(algebra/cubic_discriminant): add nat degree and monic lemmas (#17780) Relocate leading coeff lemmas to coeff section.

Estimated changes

Modified src/algebra/cubic_discriminant.lean

added theorem cubic.monic_of_a_eq_one'

added theorem cubic.monic_of_a_eq_one

added theorem cubic.monic_of_b_eq_one'

added theorem cubic.monic_of_b_eq_one

added theorem cubic.monic_of_c_eq_one'

added theorem cubic.monic_of_c_eq_one

added theorem cubic.monic_of_d_eq_one'

added theorem cubic.monic_of_d_eq_one

added theorem cubic.nat_degree_of_a_eq_zero'

added theorem cubic.nat_degree_of_a_eq_zero

added theorem cubic.nat_degree_of_a_ne_zero'

added theorem cubic.nat_degree_of_a_ne_zero

added theorem cubic.nat_degree_of_b_eq_zero'

added theorem cubic.nat_degree_of_b_eq_zero

added theorem cubic.nat_degree_of_b_ne_zero'

added theorem cubic.nat_degree_of_b_ne_zero

added theorem cubic.nat_degree_of_c_eq_zero'

added theorem cubic.nat_degree_of_c_eq_zero

added theorem cubic.nat_degree_of_c_ne_zero'

added theorem cubic.nat_degree_of_c_ne_zero

added theorem cubic.nat_degree_of_zero