Theorem AnalyticWithinAt.smul

Modification history

2026-01-29 18:03

Mathlib/Analysis/Analytic/Constructions.lean

feat(Analysis/Analytic, Analysis/Calculus): allow more general types in SMul (#34515) …

Modified AnalyticWithinAt.smul View on Github →

2024-09-16 17:23

Mathlib/Analysis/Analytic/Constructions.lean

feat: more API for `AnalyticWithinAt` (#16843) …

Added AnalyticWithinAt.smul View on Github →