# Documentation

Mathlib.Algebra.Polynomial.GroupRingAction

# 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.instMulSemiringActionPolynomialSemiring (M : Type u_1) [] (R : Type u_2) [] [] :
@[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.

Instances For
theorem prodXSubSmul.monic (G : Type u_2) [] [] (R : Type u_3) [] [] (x : R) :
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 : ) :
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.

Instances For
@[simp]
theorem MulSemiringActionHom.coe_polynomial {M : Type u_1} [] {P : Type u_2} [] [] {Q : Type u_3} [] [] (g : P →+*[M] Q) :