Theorem set_smul_mem_nhds_smul_iff

Modification history

2024-08-09 02:03
Mathlib/Topology/Algebra/ConstMulAction.lean
feat(Topology/Algebra): add `smul_mem_nhds_smul` (#15563) …
Deleted set_smul_mem_nhds_smul_iffView on Github →
2023-02-02 17:16
Mathlib/Topology/Algebra/ConstMulAction.lean
feat: port Topology.Algebra.ConstMulAction (#2012)
Added set_smul_mem_nhds_smul_iffView on Github →