Theorem CPolynomialAt.fun_comp_of_eq

Modification history

2026-06-04 08:41
Mathlib/Analysis/Analytic/Composition.lean
chore: use `to_fun` to auto-generated eta-expanded versions of `comp` declarations (#34361) …
Deleted CPolynomialAt.fun_comp_of_eqView on Github →
2025-10-01 09:41
Mathlib/Analysis/Analytic/Composition.lean
feat: the composition of continuously polynomial functions is continuously polynomial (#30086)
Added CPolynomialAt.fun_comp_of_eqView on Github →