mathlib documentation

algebra.polynomial.group_ring_action

Group action on rings applied to polynomials #

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] [mul_semiring_action M R] (m : M) :
@[protected, instance]
noncomputable def polynomial.mul_semiring_action (M : Type u_1) [monoid M] (R : Type u_2) [semiring R] [mul_semiring_action M R] :
Equations
@[simp]
theorem polynomial.smul_X {M : Type u_1} [monoid M] {R : Type u_2} [semiring R] [mul_semiring_action M R] (m : M) :
theorem polynomial.smul_eval_smul {M : Type u_1} [monoid M] (S : Type u_3) [comm_semiring S] [mul_semiring_action M S] (m : M) (f : polynomial S) (x : S) :
theorem polynomial.eval_smul' (S : Type u_3) [comm_semiring S] (G : Type u_4) [group G] [mul_semiring_action G S] (g : G) (f : polynomial S) (x : S) :
theorem polynomial.smul_eval (S : Type u_3) [comm_semiring S] (G : Type u_4) [group G] [mul_semiring_action G S] (g : G) (f : polynomial S) (x : S) :
noncomputable def prod_X_sub_smul (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [mul_semiring_action G 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] [mul_semiring_action G R] (x : R) :
theorem prod_X_sub_smul.eval (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [mul_semiring_action G R] (x : R) :
theorem prod_X_sub_smul.smul (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [mul_semiring_action G R] (x : R) (g : G) :
theorem prod_X_sub_smul.coeff (G : Type u_2) [group G] [fintype G] (R : Type u_3) [comm_ring R] [mul_semiring_action G R] (x : R) (g : G) (n : ) :
@[protected]
noncomputable def mul_semiring_action_hom.polynomial {M : Type u_1} [monoid M] {P : Type u_2} [comm_semiring P] [mul_semiring_action M P] {Q : Type u_3} [comm_semiring Q] [mul_semiring_action M 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} [comm_semiring P] [mul_semiring_action M P] {Q : Type u_3} [comm_semiring Q] [mul_semiring_action M Q] (g : P →+*[M] Q) :