@[instance]
Equations
@[instance]
Equations
- uniform_space.completion.has_neg = {neg := uniform_space.completion.map (λ (a : α), -a)}
@[instance]
theorem
uniform_space.completion.coe_neg
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
(a : α) :
theorem
uniform_space.completion.coe_add
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
(a b : α) :
@[instance]
def
uniform_space.completion.add_group
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α] :
Equations
- uniform_space.completion.add_group = {add := has_add.add uniform_space.completion.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg uniform_space.completion.has_neg, add_left_neg := _}
@[instance]
def
uniform_space.completion.uniform_add_group
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α] :
Equations
@[instance]
def
uniform_space.completion.is_add_group_hom_coe
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α] :
theorem
uniform_space.completion.is_add_group_hom_extension
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
{β : Type v}
[uniform_space β]
[add_group β]
[uniform_add_group β]
[complete_space β]
[separated_space β]
{f : α → β}
[is_add_group_hom f] :
theorem
uniform_space.completion.is_add_group_hom_map
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
{β : Type v}
[uniform_space β]
[add_group β]
[uniform_add_group β]
{f : α → β}
[is_add_group_hom f] :
@[instance]
def
uniform_space.completion.add_comm_group
{α : Type u}
[uniform_space α]
[add_comm_group α]
[uniform_add_group α] :