Theorem Filter.Tendsto.num

Modification history

2025-08-03 15:47

Mathlib/Analysis/SpecificLimits/Basic.lean

chore: fix wrong namespacing of `Tendsto.num` (#27893) …

Added Filter.Tendsto.num View on Github →