Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-15 20:25 5d791c6b

View on Github →

feat(data/polynomial): nth_roots (#260)

Estimated changes

Modified data/polynomial.lean

added theorem polynomial.C_add

added theorem polynomial.C_mul

deleted theorem polynomial.C_mul_C

added theorem polynomial.X_pow_sub_C_ne_zero

added theorem polynomial.card_nth_roots

added theorem polynomial.card_roots_X_pow_sub_C

added theorem polynomial.degree_X_pow

added theorem polynomial.degree_X_pow_sub_C

added theorem polynomial.eval_pow

added theorem polynomial.leading_coeff_X_pow

added theorem polynomial.mem_nth_roots