mathlib documentation

topology.algebra.group_completion

theorem uniform_space.completion.coe_zero {α : Type u} [uniform_space α] [has_zero α] :
0 = 0

theorem uniform_space.completion.coe_neg {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a : α) :

theorem uniform_space.completion.coe_sub {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a b : α) :
(a - b) = a - b

theorem uniform_space.completion.coe_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a b : α) :
(a + b) = a + b