Commit 2025-02-20 08:08 13b8d6bb

View on Github →

chore: split CPolynomial (#22102) Currently, CPolynomial imports Linear, but there is a TODO that Linear should be refactored in terms of CPolynomial. To revert the import order, one needs to split the original file into two parts, as done in this PR.

Estimated changes

deleted theorem CPolynomialAt.analyticAt
deleted theorem CPolynomialAt.congr
deleted def CPolynomialAt
deleted theorem CPolynomialAt_congr
deleted theorem CPolynomialOn.analyticOn
deleted theorem CPolynomialOn.congr'
deleted theorem CPolynomialOn.congr
deleted theorem CPolynomialOn.continuous
deleted theorem CPolynomialOn.mono
deleted def CPolynomialOn
deleted theorem CPolynomialOn_congr'
deleted theorem CPolynomialOn_congr
deleted structure HasFiniteFPowerSeriesOnBall
deleted theorem isOpen_cPolynomialAt
added theorem CPolynomialAt.congr
added def CPolynomialAt
added theorem CPolynomialAt_congr
added theorem CPolynomialOn.congr'
added theorem CPolynomialOn.congr
added theorem CPolynomialOn.mono
added def CPolynomialOn
added theorem CPolynomialOn_congr'
added theorem CPolynomialOn_congr
added theorem isOpen_cPolynomialAt