mathlib documentation


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

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

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

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


The completion extension as a ring morphism.


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.