Skip to content

Commit

Permalink
chore(topology): add 2 missing inhabited instances (#10446)
Browse files Browse the repository at this point in the history
Also add an instance from `discrete_topology` to `topological_ring`.
  • Loading branch information
urkud committed Nov 24, 2021
1 parent 1c00179 commit d267b6c
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 0 deletions.
4 changes: 4 additions & 0 deletions src/topology/algebra/ring.lean
Expand Up @@ -39,6 +39,10 @@ If `R` is a ring, then negation is automatically continuous, as it is multiplica
class topological_ring [topological_space α] [semiring α]
extends has_continuous_add α, has_continuous_mul α : Prop

@[priority 50]
instance discrete_topology.topological_ring {α} [topological_space α] [semiring α]
[discrete_topology α] : topological_ring α := ⟨⟩

section
variables {α} [topological_space α] [semiring α] [topological_ring α]

Expand Down
2 changes: 2 additions & 0 deletions src/topology/category/Top/open_nhds.lean
Expand Up @@ -60,6 +60,8 @@ instance (x : X) : order_top (open_nhds x) :=
{ top := ⟨⊤, trivial⟩,
le_top := λ _, le_top }

instance (x : X) : inhabited (open_nhds x) := ⟨⊤⟩

instance open_nhds_category (x : X) : category.{u} (open_nhds x) :=
by {unfold open_nhds, apply_instance}

Expand Down
2 changes: 2 additions & 0 deletions src/topology/category/TopCommRing.lean
Expand Up @@ -27,6 +27,8 @@ structure TopCommRing :=

namespace TopCommRing

instance : inhabited TopCommRing := ⟨⟨punit⟩⟩

instance : has_coe_to_sort TopCommRing (Type u) := ⟨TopCommRing.α⟩

attribute [instance] is_comm_ring is_topological_space is_topological_ring
Expand Down

0 comments on commit d267b6c

Please sign in to comment.