Skip to content

Commit

Permalink
chore(topology/algebra/group_with_zero): mark has_continuous_inv₀ a…
Browse files Browse the repository at this point in the history
…s a `Prop` (#12770)

Since the type was not explicitly given, Lean marked this as a `Type`.
  • Loading branch information
j-loreaux committed Mar 17, 2022
1 parent 3e6e34e commit 2cb5edb
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/topology/algebra/group_with_zero.lean
Expand Up @@ -73,7 +73,7 @@ end div_const

/-- A type with `0` and `has_inv` such that `λ x, x⁻¹` is continuous at all nonzero points. Any
normed (semi)field has this property. -/
class has_continuous_inv₀ (G₀ : Type*) [has_zero G₀] [has_inv G₀] [topological_space G₀] :=
class has_continuous_inv₀ (G₀ : Type*) [has_zero G₀] [has_inv G₀] [topological_space G₀] : Prop :=
(continuous_at_inv₀ : ∀ ⦃x : G₀⦄, x ≠ 0 → continuous_at has_inv.inv x)

export has_continuous_inv₀ (continuous_at_inv₀)
Expand Down

0 comments on commit 2cb5edb

Please sign in to comment.