Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-16 08:10 5120cf49

View on Github →

chore(data/mv_polynomial): reverse an import (#18593) As proposed on zulip

Estimated changes

Modified src/data/mv_polynomial/monad.lean

added theorem mv_polynomial.mem_vars_bind₁

added theorem mv_polynomial.vars_bind₁

Modified src/data/mv_polynomial/variables.lean

deleted theorem mv_polynomial.mem_vars_bind₁

deleted theorem mv_polynomial.vars_bind₁

Modified src/ring_theory/polynomial/quotient.lean