Commit 2023-03-14 07:26 c1fa0cc8

View on Github →

feat: port Algebra.Polynomial.GroupRingAction (#2863)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Polynomial/GroupRingAction.lean

added theorem MulSemiringActionHom.coe_polynomial

added theorem Polynomial.eval_smul'

added theorem Polynomial.smul_X

added theorem Polynomial.smul_eq_map

added theorem Polynomial.smul_eval

added theorem Polynomial.smul_eval_smul

added theorem prodXSubSmul.coeff

added theorem prodXSubSmul.eval

added theorem prodXSubSmul.monic

added theorem prodXSubSmul.smul