Commit 2022-03-31 06:51 760f1b2b

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, 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.

• depends on: #12748