Documentation

Mathlib.Algebra.Polynomial.GroupRingAction

Group action on rings applied to polynomials #

This file contains instances and definitions relating MulSemiringAction to Polynomial.

@[simp]
theorem Polynomial.smul_X {M : Type u_1} [Monoid M] {R : Type u_2} [Semiring R] [MulSemiringAction M R] (m : M) :
m Polynomial.X = Polynomial.X
theorem Polynomial.smul_eval_smul {M : Type u_1} [Monoid M] (S : Type u_3) [CommSemiring S] [MulSemiringAction M S] (m : M) (f : Polynomial S) (x : S) :
theorem Polynomial.eval_smul' (S : Type u_3) [CommSemiring S] (G : Type u_4) [Group G] [MulSemiringAction G S] (g : G) (f : Polynomial S) (x : S) :
theorem Polynomial.smul_eval (S : Type u_3) [CommSemiring S] (G : Type u_4) [Group G] [MulSemiringAction G S] (g : G) (f : Polynomial S) (x : S) :
noncomputable def prodXSubSMul (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) :

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

Equations
Instances For
    theorem prodXSubSMul.monic (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) :
    (prodXSubSMul G R x).Monic
    theorem prodXSubSMul.eval (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) :
    theorem prodXSubSMul.smul (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) (g : G) :
    theorem prodXSubSMul.coeff (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (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} [Monoid M] {P : Type u_2} [CommSemiring P] [MulSemiringAction M P] {Q : Type u_3} [CommSemiring Q] [MulSemiringAction M Q] (g : P →+*[M] Q) :

    An equivariant map induces an equivariant map on polynomials.

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