Group action on rings applied to polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains instances and definitions relating
the product of
(X - g • x) over distinct
g • x.
An equivariant map induces an equivariant map on polynomials.