mathlib documentation

topology.algebra.group_completion

@[instance]

def uniform_space.completion.has_zero {α : Type u} [uniform_space α] [has_zero α] :

has_zero (uniform_space.completion α)

Equations

uniform_space.completion.has_zero = {zero := ↑0}

@[instance]

def uniform_space.completion.has_neg {α : Type u} [uniform_space α] [has_neg α] :

has_neg (uniform_space.completion α)

Equations

uniform_space.completion.has_neg = {neg := uniform_space.completion.map (λ (a : α), -a)}

@[instance]

def uniform_space.completion.has_add {α : Type u} [uniform_space α] [has_add α] :

has_add (uniform_space.completion α)

Equations

uniform_space.completion.has_add = {add := uniform_space.completion.map₂ has_add.add}

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_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a b : α) :

↑(a + b) = ↑a + ↑b

@[instance]

def uniform_space.completion.add_group {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :

add_group (uniform_space.completion α)

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 α] :

uniform_add_group (uniform_space.completion α)

@[instance]

def uniform_space.completion.is_add_group_hom_coe {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :

is_add_group_hom coe

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] (hf : continuous f) :

is_add_group_hom (uniform_space.completion.extension 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] (hf : continuous f) :

is_add_group_hom (uniform_space.completion.map f)

@[instance]

def uniform_space.completion.add_comm_group {α : Type u} [uniform_space α] [add_comm_group α] [uniform_add_group α] :

add_comm_group (uniform_space.completion α)

Equations

uniform_space.completion.add_comm_group = {add := add_group.add uniform_space.completion.add_group, add_assoc := _, zero := add_group.zero uniform_space.completion.add_group, zero_add := _, add_zero := _, neg := add_group.neg uniform_space.completion.add_group, add_left_neg := _, add_comm := _}