Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 09:30 3a5c8711

View on Github →

refactor(polynomial/*): make polynomials irreducible (#7421) Polynomials are the most basic objects in field theory. Making them irreducible helps Lean, because it can not try to unfold things too far, and it helps the user because it forces him to use a sane API instead of mixing randomly stuff from finsupp and from polynomials, as used to be the case in mathlib before this PR.

Estimated changes

modified def polynomial.C
modified theorem polynomial.C_0
modified def polynomial.coeff
added theorem polynomial.coeff_erase
deleted theorem polynomial.coeff_mk
modified theorem polynomial.coeff_neg
modified theorem polynomial.coeff_one_zero
modified theorem polynomial.coeff_sub
added theorem polynomial.erase_ne
added theorem polynomial.erase_same
added theorem polynomial.erase_zero
modified def polynomial.monomial
deleted theorem polynomial.monomial_def
added def polynomial.sum
modified theorem polynomial.sum_C_index
added theorem polynomial.sum_X_index
added theorem polynomial.sum_add'
added theorem polynomial.sum_add
added theorem polynomial.sum_def
modified def polynomial.support
modified theorem polynomial.support_add
modified theorem polynomial.support_zero
added structure polynomial
deleted def polynomial
modified theorem polynomial.coeff_add
deleted theorem polynomial.sum_def
modified theorem polynomial.degree_C_le
deleted theorem polynomial.degree_map_le
modified theorem polynomial.eval_eq_sum
modified theorem polynomial.mirror_zero
deleted theorem polynomial.C_mul_monomial
deleted theorem polynomial.monomial_mul_C
modified theorem polynomial.coeff_contract
modified theorem polynomial.coeff_to_subring
added theorem polynomial.frange_one
added theorem polynomial.frange_zero
modified theorem polynomial.restriction_zero
modified theorem polynomial.to_subring_zero