Commit 2022-08-09 04:12 0bd4faee

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.