Theorem FormalMultilinearSeries.radius_unshift

Modification history

2025-08-16 00:05
Mathlib/Analysis/Analytic/Basic.lean
chore(Analysis/Analytic): split `Analytic.Basic` (#26270) …
Modified FormalMultilinearSeries.radius_unshiftView on Github →
2024-12-18 06:37
Mathlib/Analysis/Analytic/Basic.lean
feat(Analysis/Analytic): `FormalMultilinearSeries.unshift` convergence (#19848) …
Added FormalMultilinearSeries.radius_unshiftView on Github →