Commit 2025-11-26 05:44 46c21b00

feat(Algebra/Polynomial/Factors): Composition with negation of X is multiplicative (#32121) This PR proves (p * q).comp (-X) = p.comp (-X) * q.comp (-X) for rings (possibly noncommutative) and deduces that f.Splits implies (f.comp (-X)).Splits. This generalizes the current theorem Polynomial.Splits.comp_neg_X so that the coefficients may be taken from a Ring instead of a Field