Commit 2024-11-17 16:01 62ee20ff

View on Github →

feat(Polynomial): composing with the constant polynomial (#19090) ... and a point-free version of coeff_map From GrowthInGroups

Estimated changes

Modified Mathlib/Algebra/Polynomial/Eval/Coeff.lean

added theorem Polynomial.coeff_map_eq_comp

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

added theorem Polynomial.mapRingHom_comp_C