Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-06 09:02 c08a8686

View on Github →

feat(trailing_degree): added two lemmas support_X, support_X_empty computing the support of X, simplified a couple of lemmas (#4294)

Estimated changes

Modified src/data/polynomial/basic.lean

added theorem polynomial.monomial_eq_X_pow

added theorem polynomial.support_X

added theorem polynomial.support_X_empty

added theorem polynomial.support_X_pow

added theorem polynomial.support_monomial'

added theorem polynomial.support_monomial

Modified src/data/polynomial/coeff.lean

added theorem polynomial.C_mul_X_pow_eq_monomial

deleted theorem polynomial.monomial_eq_smul_X

deleted theorem polynomial.monomial_one_eq_X_pow

added theorem polynomial.support_C_mul_X_pow'

added theorem polynomial.support_mul_X_pow

Modified src/data/polynomial/degree/trailing_degree.lean

modified theorem polynomial.trailing_degree_lt_wf

Modified src/data/polynomial/monomial.lean

added theorem polynomial.monomial_eq_smul_X

added theorem polynomial.monomial_one_eq_X_pow