Commit 2021-01-15 16:03 8b4b9413

View on Github →

feat(data/mv_polynomial): stronger degrees_X for nontrivial R (#5758) Also rename degrees_X to degrees_X' and mark degrees_{zero,one} with simp.

Estimated changes

Modified src/data/mv_polynomial/variables.lean

added theorem mv_polynomial.degrees_X'

modified theorem mv_polynomial.degrees_X

modified theorem mv_polynomial.degrees_one

modified theorem mv_polynomial.degrees_zero

Modified src/field_theory/finite/polynomial.lean