Description: Define a topological division ring (which differs from a topological field
only in being potentially noncommutative), which is a division ring and
topological ring such that the unit group of the division ring (which is
the set of nonzero elements) is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015)