mathlib3

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

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.