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.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
