Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-05 09:08 600d3cf6

View on Github →

cleanup(data/polynomial): shorten some proofs

Estimated changes

Modified data/finsupp.lean

added theorem finsupp.support_add_eq

Modified data/polynomial.lean

added theorem polynomial.apply_nat_degree_eq_zero_of_degree_lt

added theorem polynomial.degree_le_degree

added theorem polynomial.degree_le_nat_degree

added theorem polynomial.le_nat_degree_of_ne_zero