Commit 2023-01-11 01:12 3879543c

feat(topology/algebra/monoid): add lemmas about 𝓝 a * 𝓝 b (#18099)

• Add le_nhds_mul, nhds_one_mul_nhds, nhds_mul_nhds_one, map_mul_right_nhds, and map_mul_right_nhds_one.
• Golf nhds_mul and generalize it to noncommutative groups.