chore(topology/algebra/group_with_zero): fix docstring for has_contin…

…uous_inv0 (#12653)

src/topology/algebra/group_with_zero.lean

@@ -10,9 +10,9 @@ import topology.homeomorph
 /-!
 # Topological group with zero
 
-In this file we define `has_continuous_inv'` to be a mixin typeclass a type with `has_inv` and
+In this file we define `has_continuous_inv₀` to be a mixin typeclass a type with `has_inv` and
 `has_zero` (e.g., a `group_with_zero`) such that `λ x, x⁻¹` is continuous at all nonzero points. Any
-normed (semi)field has this property. Currently the only example of `has_continuous_inv'` in
+normed (semi)field has this property. Currently the only example of `has_continuous_inv₀` in
 `mathlib` which is not a normed field is the type `nnnreal` (a.k.a. `ℝ≥0`) of nonnegative real
 numbers.
 
@@ -22,7 +22,7 @@ and `continuous`. As a special case, we provide `*.div_const` operations that re
 `group_with_zero` and `has_continuous_mul` instances.
 
 All lemmas about `(⁻¹)` use `inv'` in their names because lemmas without `'` are used for
-`topological_group`s. We also use `'` in the typeclass name `has_continuous_inv'` for the sake of
+`topological_group`s. We also use `'` in the typeclass name `has_continuous_inv₀` for the sake of
 consistency of notation.
 
 On a `group_with_zero` with continuous multiplication, we also define left and right multiplication

src/topology/instances/nnreal.lean

@@ -20,7 +20,7 @@ Instances for the following typeclasses are defined:
 * `second_countable_topology ℝ≥0`
 * `order_topology ℝ≥0`
 * `has_continuous_sub ℝ≥0`
-* `has_continuous_inv' ℝ≥0` (continuity of `x⁻¹` away from `0`)
+* `has_continuous_inv₀ ℝ≥0` (continuity of `x⁻¹` away from `0`)
 * `has_continuous_smul ℝ≥0 ℝ`
 
 Everything is inherited from the corresponding structures on the reals.