Algebra towers for multivariate polynomial #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file proves some basic results about the algebra tower structure for the type
mv_polynomial σ R.
This structure itself is provided elsewhere as
When you update this file, you can also try to make a corresponding update in