Theorem Filter.tendsto_const_mul_iff

Modification history

2026-02-16 15:42
Mathlib/Topology/Algebra/Group/Basic.lean
feat: review lemmas about tendsto and group operations (#34792) …
Added Filter.tendsto_const_mul_iffView on Github →