Commit 2024-08-09 02:03 1339db17

feat(Topology/Algebra): add smul_mem_nhds_smul (#15563)

• add smul_mem_nhds_smul_iff and smul_mem_nhds_smul, deprecate smul_mem_nhds;
• move 3 lemmas up in the import graph;
• add smul_mem_nhds_self;
• rename set_smul_mem_nhds_smul_iff to smul_mem_nhds_smul_iff₀, deprecate the old lemma;
• similarly with set_smul_mem_nhds_smul and smul_mem_nhds_smul₀;