Theorem FormalMultilinearSeries.zero_radius

Modification history

2025-08-16 00:05
Mathlib/Analysis/Analytic/Basic.lean
chore(Analysis/Analytic): split `Analytic.Basic` (#26270) …
Modified FormalMultilinearSeries.zero_radiusView on Github →
2024-06-19 11:32
Mathlib/Analysis/Analytic/Basic.lean
feat: add a few analytic function lemmas for future AnalyticManifold use (#13784) …
Added FormalMultilinearSeries.zero_radiusView on Github →