Commit 2023-04-04 22:00 3b1890e7

chore(topology/algebra/group): generalise instances (#15171) Using the generalisation linter make the following generalisations in topology.algebra.group.basic. Note that topological spaces that are groups with continuous multiplication but noncontinuous inverse do exist at least when the space is noncompact (they are known as paratopological spaces) I do not claim that they are used in mathlib though ;). In summary we generalise:

• tendsto_inv_nhds_within_Ioi and all variants to only require continuous inverse rather that topological group
• the continuous_inv operation on the multiplicative opposite to only require a has_inv, rather than a group
• topological_group.t1_space from topological groups to only continuous mul
• topological_group.regular_space (and t2_space) from assuming the base is t1 to just topological group.
• compact_open_separated_mul_right/left, from topological group to mul_one_class with a continuous mul
• various quotient_group.has_continuous_const_smul type lemmas to continuous_mul
• tsum_sigma/tsum_prod from t1 to t0 and their additivised versions.