mathlib3

e23b97e5 - feat(ring_theory/polynomial): decomposing the kernel of an endomorphism polynomial (#4174)