# mathlibdocumentation

topology.algebra.ring

@[class]
structure topological_semiring (α : Type u) [semiring α] :
Prop
• to_has_continuous_mul :

A topological semiring is a semiring where addition and multiplication are continuous.

Instances
@[class]
structure topological_ring (α : Type u) [ring α] :
Prop
• to_has_continuous_mul :
• continuous_neg : continuous (λ (a : α), -a)

A topological ring is a ring where the ring operations are continuous.

Instances
@[instance]

@[instance]

theorem mul_left_continuous {α : Type u} [ring α] (x : α) :

In a topological ring, the left-multiplication add_monoid_hom is continuous.

theorem mul_right_continuous {α : Type u} [ring α] (x : α) :

In a topological ring, the right-multiplication add_monoid_hom is continuous.

def ideal.closure {α : Type u_1} [comm_ring α]  :

The closure of an ideal in a topological ring as an ideal.

Equations
@[simp]
theorem ideal.coe_closure {α : Type u_1} [comm_ring α] (S : ideal α) :

@[instance]
def topological_ring_quotient_topology {α : Type u_1} [comm_ring α] (N : ideal α) :

Equations
theorem quotient_ring_saturate {α : Type u_1} [comm_ring α] (N : ideal α) (s : set α) :
⁻¹' ( '' s) = ⋃ (x : N), (λ (y : α), x.val + y) '' s

theorem quotient_ring.is_open_map_coe {α : Type u_1} [comm_ring α] (N : ideal α)  :

theorem quotient_ring.quotient_map_coe_coe {α : Type u_1} [comm_ring α] (N : ideal α)  :
quotient_map (λ (p : α × α), ( p.fst, p.snd))

@[instance]
def topological_ring_quotient {α : Type u_1} [comm_ring α] (N : ideal α)  :