mathlib

760f1b2b - refactor(*): rename `topological_ring` to `topological_semiring` and introduce a new `topological_ring` extending `has_continuous_neg` (#12864)

refactor(*): rename `topological_ring` to `topological_semiring` and introduce a new `topological_ring` extending `has_continuous_neg` (#12864) Following the discussion in this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/continuous.20maps.20vanishing.20at.20infinity/near/275553306), this renames `topological_ring` to `topological_semiring` throughout the library and weakens the typeclass assumptions from `semiring` to `non_unital_non_assoc_semiring`. Moreover, it introduces a new `topological_ring` class which takes a type class parameter of `non_unital_non_assoc_ring` and extends `topological_semiring` and `has_continuous_neg`. In the case of *unital* (semi)rings (even non-associative), the type class `topological_semiring` is sufficient to capture the notion of `topological_ring` because negation is just multiplication by `-1`. Therefore, those working with unital (semi)rings can proceed with the small change of using `topological_semiring` instead of `topological_ring`. The primary reason for the distinction is to weaken the type class assumptions to allow for non-unital rings, in which case `has_continuous_neg` must be explicitly assumed. - [x] depends on: #12748 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>