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.

@[simp]
theorem polynomial.coeff_smul' {M : Type u_1} [monoid M] {R : Type u_2} [semiring R] [mul_semiring_action M R] (m : M) (p : polynomial R) (n : ) :
(m p).coeff n = m p.coeff n

@[simp]
theorem polynomial.smul_C {M : Type u_1} [monoid M] {R : Type u_2} [semiring R] [mul_semiring_action M R] (m : M) (r : R) :

@[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) :

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 : ) :

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) :