Commit 2025-03-10 19:32 4164c7be

View on Github →

chore: cleanup names in CPolynomial (#22789)

Estimated changes

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

modified theorem ContinuousMultilinearMap.analyticOnNhd

added theorem ContinuousMultilinearMap.cpolynomialOn

deleted theorem ContinuousMultilinearMap.cpolyomialOn

Modified Mathlib/Analysis/Analytic/CPolynomialDef.lean

deleted theorem CPolynomialAt.eventually_cPolynomialAt

added theorem CPolynomialAt.eventually_cpolynomialAt

deleted theorem CPolynomialAt.exists_ball_cPolynomialOn

added theorem CPolynomialAt.exists_ball_cpolynomialOn

deleted theorem CPolynomialAt.exists_mem_nhds_cPolynomialOn

added theorem CPolynomialAt.exists_mem_nhds_cpolynomialOn

deleted theorem ContinuousLinearMap.comp_cPolynomialOn

added theorem ContinuousLinearMap.comp_cpolynomialOn

deleted theorem FormalMultilinearSeries.cPolynomialAt_changeOrigin_of_finite

added theorem FormalMultilinearSeries.cpolynomialAt_changeOrigin_of_finite

deleted theorem HasFiniteFPowerSeriesAt.cPolynomialAt

added theorem HasFiniteFPowerSeriesAt.cpolynomialAt

added theorem HasFiniteFPowerSeriesAt.hasFPowerSeriesAt

added theorem HasFiniteFPowerSeriesAt.of_le

deleted theorem HasFiniteFPowerSeriesAt.toHasFPowerSeriesAt

deleted theorem HasFiniteFPowerSeriesOnBall.cPolynomialAt

deleted theorem HasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem

deleted theorem HasFiniteFPowerSeriesOnBall.cPolynomialOn

added theorem HasFiniteFPowerSeriesOnBall.cpolynomialAt

added theorem HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem

added theorem HasFiniteFPowerSeriesOnBall.cpolynomialOn

added theorem HasFiniteFPowerSeriesOnBall.of_le

deleted theorem isOpen_cPolynomialAt

added theorem isOpen_cpolynomialAt

Modified Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

deleted theorem ContinuousMultilinearMap.cPolynomialAt

deleted theorem ContinuousMultilinearMap.cPolyomialOn