# mathlibdocumentation

topology.algebra.uniform_ring

@[instance]
def uniform_space.completion.has_one (α : Type u_1) [ring α]  :

Equations
@[instance]
def uniform_space.completion.has_mul (α : Type u_1) [ring α]  :

Equations
theorem uniform_space.completion.coe_one (α : Type u_1) [ring α]  :
1 = 1

theorem uniform_space.completion.coe_mul {α : Type u_1} [ring α] (a b : α) :
a * b = (a) * b

theorem uniform_space.completion.continuous_mul {α : Type u_1} [ring α]  :
continuous (λ (p : , (p.fst) * p.snd)

theorem uniform_space.completion.continuous.mul {α : Type u_1} [ring α] {β : Type u_2} {f g : β → } :
continuous (λ (b : β), (f b) * g b)

@[instance]
def uniform_space.completion.ring {α : Type u_1} [ring α]  :

Equations
def uniform_space.completion.coe_ring_hom {α : Type u_1} [ring α]  :

The map from a uniform ring to its completion, as a ring homomorphism.

Equations
def uniform_space.completion.extension_hom {α : Type u_1} [ring α] {β : Type u} [ring β] (f : α →+* β) (hf : continuous f)  :

The completion extension as a ring morphism.

Equations
@[instance]
def uniform_space.completion.top_ring_compl {α : Type u_1} [ring α]  :

def uniform_space.completion.map_ring_hom {α : Type u_1} [ring α] {β : Type u} [ring β] (f : α →+* β) :

The completion map as a ring morphism.

Equations
@[instance]
def uniform_space.completion.comm_ring (R : Type u_2) [comm_ring R]  :

Equations
theorem uniform_space.ring_sep_rel (α : Type u_1) [comm_ring α]  :

theorem uniform_space.ring_sep_quot (α : Type u_1) [r : comm_ring α]  :

def uniform_space.sep_quot_equiv_ring_quot (α : Type u_1) [r : comm_ring α]  :

Given a topological ring α equipped with a uniform structure that makes subtraction uniformly continuous, get an equivalence between the separated quotient of α and the quotient ring corresponding to the closure of zero.

Equations
@[instance]
def uniform_space.comm_ring {α : Type u_1} [comm_ring α]  :

Equations
@[instance]
def uniform_space.topological_ring {α : Type u_1} [comm_ring α]  :