mathlib3
8b4b9413 - feat(data/mv_polynomial): stronger `degrees_X` for `nontrivial R` (#5758)

Commit

5 years ago

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`.

Author

eric-wieser

Parents

c347c75d

mathlib3 8b4b9413 - feat(data/mv_polynomial): stronger `degrees_X` for `nontrivial R` (#5758)

mathlib3
8b4b9413 - feat(data/mv_polynomial): stronger `degrees_X` for `nontrivial R` (#5758)