Commit 2020-11-05 17:06 6a1ce57b

View on Github →

chore(algebra/module/linear_map): Derive linear_map from mul_action_hom (#4888) Note that this required some stuff about polynomials to move to cut import cycles.

Estimated changes

Modified src/algebra/group_action_hom.lean

deleted theorem mul_semiring_action_hom.coe_polynomial

Modified src/algebra/group_ring_action.lean

deleted theorem polynomial.coeff_smul'

deleted theorem polynomial.eval_smul'

deleted theorem polynomial.smul_C

deleted theorem polynomial.smul_X

deleted theorem polynomial.smul_eval

deleted theorem polynomial.smul_eval_smul

deleted theorem prod_X_sub_smul.coeff

deleted theorem prod_X_sub_smul.eval

deleted theorem prod_X_sub_smul.monic

deleted theorem prod_X_sub_smul.smul

Modified src/algebra/module/linear_map.lean

Created src/algebra/polynomial/group_ring_action.lean

added theorem mul_semiring_action_hom.coe_polynomial

added theorem polynomial.coeff_smul'

added theorem polynomial.eval_smul'

added theorem polynomial.smul_C

added theorem polynomial.smul_X

added theorem polynomial.smul_eval

added theorem polynomial.smul_eval_smul

added theorem prod_X_sub_smul.coeff

added theorem prod_X_sub_smul.eval

added theorem prod_X_sub_smul.monic

added theorem prod_X_sub_smul.smul

Modified src/field_theory/fixed.lean

Modified src/group_theory/sylow.lean