Commit 2023-03-28 10:43 7fb2ff36

View on Github →

feat: port Algebra.CubicDiscriminant (#3142)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CubicDiscriminant.lean

added theorem Cubic.C_mul_prod_X_sub_C_eq

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

added theorem Cubic.d_eq_three_roots

added theorem Cubic.d_of_eq

added theorem Cubic.degree_of_a_eq_zero'

added 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

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 def Cubic.equiv

added theorem Cubic.leadingCoeff_of_a_ne_zero'

added theorem Cubic.leadingCoeff_of_a_ne_zero

added theorem Cubic.leadingCoeff_of_b_ne_zero'

added theorem Cubic.leadingCoeff_of_b_ne_zero

added theorem Cubic.leadingCoeff_of_c_eq_zero'

added theorem Cubic.leadingCoeff_of_c_eq_zero

added theorem Cubic.leadingCoeff_of_c_ne_zero'

added theorem Cubic.leadingCoeff_of_c_ne_zero

added def Cubic.map

added theorem Cubic.map_roots

added theorem Cubic.map_toPoly

added theorem Cubic.mem_roots_iff

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

added theorem Cubic.natDegree_of_a_eq_zero

added theorem Cubic.natDegree_of_a_ne_zero'

added theorem Cubic.natDegree_of_a_ne_zero

added theorem Cubic.natDegree_of_b_eq_zero'

added theorem Cubic.natDegree_of_b_eq_zero

added theorem Cubic.natDegree_of_b_ne_zero'

added theorem Cubic.natDegree_of_b_ne_zero

added theorem Cubic.natDegree_of_c_eq_zero'

added theorem Cubic.natDegree_of_c_eq_zero

added theorem Cubic.natDegree_of_c_ne_zero'

added theorem Cubic.natDegree_of_c_ne_zero

added theorem Cubic.natDegree_of_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_eq_zero'

added 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

added theorem Cubic.prod_X_sub_C_eq

added def Cubic.roots

added theorem Cubic.splits_iff_card_roots

added theorem Cubic.splits_iff_roots_eq_three

added def Cubic.toPoly

added theorem Cubic.toPoly_eq_zero_iff

added theorem Cubic.toPoly_injective

added theorem Cubic.zero

added structure Cubic