mathlib3

0bd4faee - feat(topology/algebra/group): add lemmas about `units` (#15921)

feat(topology/algebra/group): add lemmas about `units` (#15921) * add `simps` attribute here and there; * add `continuous_prod_mk`, `units.continuous_iff`, `units.continuous_inv`, and `continuous.map_units`; * golf `homeomorph.prod_units`, add additive version; * drop unused section variables, golf `topological_group_Inf`.