mathlib

5ecd27ad - refactor(topology/algebra/field): make `topological_division_ring` extend `has_continuous_inv₀` (#12778)

refactor(topology/algebra/field): make `topological_division_ring` extend `has_continuous_inv₀` (#12778) Topological division ring had been rolling its own `continuous_inv` field which was almost identical to the `continuous_at_inv₀` field of `has_continuous_inv₀`. Here we refactor so that `topological_division_ring` extends `has_continuous_inv₀` instead. - [x] depends on: #12770