Theorem smul_mem_nhds_self

Modification history

2024-08-09 02:03
Mathlib/Topology/Algebra/ConstMulAction.lean
feat(Topology/Algebra): add `smul_mem_nhds_smul` (#15563) …
Added smul_mem_nhds_selfView on Github →