# mathlib3documentation

algebra.polynomial.group_ring_action

# 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 mul_semiring_action to polynomial.

theorem polynomial.smul_eq_map {M : Type u_1} [monoid M] (R : Type u_2) [semiring R] [ R] (m : M) :
@[protected, instance]
noncomputable def polynomial.mul_semiring_action (M : Type u_1) [monoid M] (R : Type u_2) [semiring R] [ R] :
Equations
@[simp]
theorem polynomial.smul_X {M : Type u_1} [monoid M] {R : Type u_2} [semiring R] [ R] (m : M) :
theorem polynomial.smul_eval_smul {M : Type u_1} [monoid M] (S : Type u_3) [ S] (m : M) (f : polynomial S) (x : S) :
polynomial.eval (m x) (m f) = m
theorem polynomial.eval_smul' (S : Type u_3) (G : Type u_4) [group G] [ S] (g : G) (f : polynomial S) (x : S) :
polynomial.eval (g x) f = g (g⁻¹ f)
theorem polynomial.smul_eval (S : Type u_3) (G : Type u_4) [group G] [ S] (g : G) (f : polynomial S) (x : S) :
(g f) = g polynomial.eval (g⁻¹ x) f
noncomputable def prod_X_sub_smul (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [ R] (x : R) :

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

Equations
theorem prod_X_sub_smul.monic (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [ R] (x : R) :
R x).monic
theorem prod_X_sub_smul.eval (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [ R] (x : R) :
R x) = 0
theorem prod_X_sub_smul.smul (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [ R] (x : R) (g : G) :
g x = x
theorem prod_X_sub_smul.coeff (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [ R] (x : R) (g : G) (n : ) :
g R x).coeff n = R x).coeff n
@[protected]
noncomputable def mul_semiring_action_hom.polynomial {M : Type u_1} [monoid M] {P : Type u_2} [ P] {Q : Type u_3} [ Q] (g : P →+*[M] Q) :

An equivariant map induces an equivariant map on polynomials.

Equations
@[simp]
theorem mul_semiring_action_hom.coe_polynomial {M : Type u_1} [monoid M] {P : Type u_2} [ P] {Q : Type u_3} [ Q] (g : P →+*[M] Q) :