# Group action on rings applied to polynomials #

This file contains instances and definitions relating MulSemiringAction to Polynomial.

theorem Polynomial.smul_eq_map {M : Type u_1} [] (R : Type u_2) [] [] (m : M) :
noncomputable instance Polynomial.instMulSemiringAction (M : Type u_1) [] (R : Type u_2) [] [] :
Equations
• = let __src := Polynomial.distribMulAction;
@[simp]
theorem Polynomial.smul_X {M : Type u_1} [] {R : Type u_2} [] [] (m : M) :
m Polynomial.X = Polynomial.X
theorem Polynomial.smul_eval_smul {M : Type u_1} [] (S : Type u_3) [] [] (m : M) (f : ) (x : S) :
Polynomial.eval (m x) (m f) = m
theorem Polynomial.eval_smul' (S : Type u_3) [] (G : Type u_4) [] [] (g : G) (f : ) (x : S) :
theorem Polynomial.smul_eval (S : Type u_3) [] (G : Type u_4) [] [] (g : G) (f : ) (x : S) :
noncomputable def prodXSubSMul (G : Type u_2) [] [] (R : Type u_3) [] [] (x : R) :

the product of (X - g • x) over distinct g • x.

Equations
• prodXSubSMul G R x = Finset.univ.prod fun (g : ) => Polynomial.X - Polynomial.C ()
Instances For
theorem prodXSubSMul.monic (G : Type u_2) [] [] (R : Type u_3) [] [] (x : R) :
(prodXSubSMul G R x).Monic
theorem prodXSubSMul.eval (G : Type u_2) [] [] (R : Type u_3) [] [] (x : R) :
theorem prodXSubSMul.smul (G : Type u_2) [] [] (R : Type u_3) [] [] (x : R) (g : G) :
theorem prodXSubSMul.coeff (G : Type u_2) [] [] (R : Type u_3) [] [] (x : R) (g : G) (n : ) :
g (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n
noncomputable def MulSemiringActionHom.polynomial {M : Type u_1} [] {P : Type u_2} [] [] {Q : Type u_3} [] [] (g : P →+*[M] Q) :

An equivariant map induces an equivariant map on polynomials.

Equations
• g.polynomial = { toFun := , map_smul' := , map_zero' := , map_add' := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem MulSemiringActionHom.coe_polynomial {M : Type u_1} [] {P : Type u_2} [] [] {Q : Type u_3} [] [] (g : P →+*[M] Q) :
g.polynomial =