@[class]
- to_has_continuous_add : has_continuous_add α
- to_has_continuous_mul : has_continuous_mul α
A topological semiring is a semiring where addition and multiplication are continuous.
@[class]
- to_has_continuous_add : has_continuous_add α
- to_has_continuous_mul : has_continuous_mul α
- continuous_neg : continuous (λ (a : α), -a)
A topological ring is a ring where the ring operations are continuous.
Instances
@[instance]
def
topological_ring.to_topological_semiring
(α : Type u)
[topological_space α]
[ring α]
[t : topological_ring α] :
Equations
@[instance]
def
topological_ring.to_topological_add_group
(α : Type u)
[topological_space α]
[ring α]
[t : topological_ring α] :
Equations
- _ = _
theorem
mul_left_continuous
{α : Type u}
[topological_space α]
[ring α]
[topological_ring α]
(x : α) :
In a topological ring, the left-multiplication add_monoid_hom is continuous.
theorem
mul_right_continuous
{α : Type u}
[topological_space α]
[ring α]
[topological_ring α]
(x : α) :
In a topological ring, the right-multiplication add_monoid_hom is continuous.
@[simp]
theorem
ideal.coe_closure
{α : Type u_1}
[topological_space α]
[comm_ring α]
[topological_ring α]
(S : ideal α) :
@[instance]
def
topological_ring_quotient_topology
{α : Type u_1}
[topological_space α]
[comm_ring α]
(N : ideal α) :
theorem
quotient_ring.is_open_map_coe
{α : Type u_1}
[topological_space α]
[comm_ring α]
(N : ideal α)
[topological_ring α] :
theorem
quotient_ring.quotient_map_coe_coe
{α : Type u_1}
[topological_space α]
[comm_ring α]
(N : ideal α)
[topological_ring α] :
quotient_map (λ (p : α × α), (⇑(ideal.quotient.mk N) p.fst, ⇑(ideal.quotient.mk N) p.snd))
@[instance]
def
topological_ring_quotient
{α : Type u_1}
[topological_space α]
[comm_ring α]
(N : ideal α)
[topological_ring α] :
Equations
- _ = _