Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-01 04:49 d3140fbe

View on Github →

feat(data/mv_polynomial): lemmas on total_degree (#2575) This is a small preparation for the Chevalley–Warning theorem.

Estimated changes

Modified src/data/mv_polynomial.lean

added theorem mv_polynomial.eval_one

added theorem mv_polynomial.eval_pow

modified theorem mv_polynomial.total_degree_C

added theorem mv_polynomial.total_degree_X

added theorem mv_polynomial.total_degree_neg

modified theorem mv_polynomial.total_degree_one

added theorem mv_polynomial.total_degree_pow

added theorem mv_polynomial.total_degree_sub

modified theorem mv_polynomial.total_degree_zero