mathlib3

6eeb54e6 - fix(topology/algebra/uniform_field): remove unnecessary topological_r… (#10614)

fix(topology/algebra/uniform_field): remove unnecessary topological_r… (#10614) …ing variable Right now the last three definitions in `topology.algebra.uniform_field` (after line 115) have `[topological_division_ring K]` and `[topological_ring K]`. For example ``` mul_hat_inv_cancel : ∀ {K : Type u_1} [_inst_1 : field K] [_inst_2 : uniform_space K] [_inst_3 : topological_division_ring K] [_inst_4 : completable_top_field K] [_inst_5 : uniform_add_group K] [_inst_6 : topological_ring K] {x : uniform_space.completion K}, x ≠ 0 → x * hat_inv x = 1 ``` Whilst it is not obvious from the notation, both of these are `Prop`s so there is no danger of diamonds. The full logic is: `field` and `uniform_space` are data, and the rest are Props (so should be called things like `is_topological_ring` etc IMO). `topological_division_ring` is the assertion of continuity of `add`, `neg`, `mul` and `inv` (away from 0), `completable_top_field` is another assertion about how inversion plays well with the topology (and which is not implied by `topological_division_ring`), `uniform_add_group` is the assertion about `add` and `neg` playing well with the uniform structure, and then `topological_ring` is a prop which is implied by `topological_division_ring`. I am not sure I see the benefits of carrying around the extra `topological_ring` for these three definitions so I've removed it to see if mathlib still compiles. Edit: it does.