Commit 2023-05-21 21:51 7b2fc8ad

View on Github →

chore: forward-port leanprover-community/mathlib#18848 (#4007) I've been someone sloppy about forward-porting the exact mathport here; a lot of the classical additions result in the whole proof being indented, which IMO just adds noise to the diff. What's important is that:

  • open Classical is removed from all the same files
  • [DecidableEq _] is added in the same position to all the same lemmas. In theory mathport will detect if we mess this up, so it's not essential to catch this in review. The linter will tell us if it is added unnecessarily, and the build will fail if is not added someewhere it is needed; so only the argument order is at risk of being wrong.
  • The new foo_def lemmas are all added in variables.lean

Estimated changes

modified theorem MvPolynomial.eval₂_add
modified theorem MvPolynomial.support_add
modified theorem MvPolynomial.support_mul
modified theorem MvPolynomial.support_sum
modified theorem MvPolynomial.degrees_sub
modified theorem MvPolynomial.support_sub
modified theorem MvPolynomial.vars_bind₁
modified theorem MvPolynomial.degreeOf_X
modified theorem MvPolynomial.degrees_add
modified theorem MvPolynomial.degrees_sum
added theorem MvPolynomial.vars_def
modified theorem MvPolynomial.vars_map
modified theorem MvPolynomial.vars_mul
modified theorem MvPolynomial.vars_prod
modified theorem MvPolynomial.vars_rename