@[instance]
Equations
- uniform_space.completion.has_one α = {one := ↑1}
@[instance]
Equations
theorem
uniform_space.completion.coe_mul
{α : Type u_1}
[ring α]
[uniform_space α]
[topological_ring α]
(a b : α) :
theorem
uniform_space.completion.continuous_mul
{α : Type u_1}
[ring α]
[uniform_space α]
[topological_ring α]
[uniform_add_group α] :
continuous (λ (p : uniform_space.completion α × uniform_space.completion α), p.fst * p.snd)
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 α} :
continuous f → continuous g → continuous (λ (b : β), f b * g b)
@[instance]
def
uniform_space.completion.ring
{α : Type u_1}
[ring α]
[uniform_space α]
[topological_ring α]
[uniform_add_group α] :
Equations
- uniform_space.completion.ring = {add := add_comm_group.add uniform_space.completion.add_comm_group, add_assoc := _, zero := add_comm_group.zero uniform_space.completion.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg uniform_space.completion.add_comm_group, add_left_neg := _, add_comm := _, mul := has_mul.mul (uniform_space.completion.has_mul α), mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
def
uniform_space.completion.coe_ring_hom
{α : Type u_1}
[ring α]
[uniform_space α]
[topological_ring α]
[uniform_add_group α] :
The map from a uniform ring to its completion, as a ring homomorphism.
Equations
- uniform_space.completion.coe_ring_hom = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
def
uniform_space.completion.extension_hom
{α : Type u_1}
[ring α]
[uniform_space α]
[topological_ring α]
[uniform_add_group α]
{β : Type u}
[uniform_space β]
[ring β]
[uniform_add_group β]
[topological_ring β]
(f : α →+* β)
(hf : continuous ⇑f)
[complete_space β]
[separated_space β] :
The completion extension as a ring morphism.
Equations
- uniform_space.completion.extension_hom f hf = have hf : uniform_continuous ⇑f, from _, {to_fun := uniform_space.completion.extension ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[instance]
def
uniform_space.completion.top_ring_compl
{α : Type u_1}
[ring α]
[uniform_space α]
[topological_ring α]
[uniform_add_group α] :
Equations
def
uniform_space.completion.map_ring_hom
{α : Type u_1}
[ring α]
[uniform_space α]
[topological_ring α]
[uniform_add_group α]
{β : Type u}
[uniform_space β]
[ring β]
[uniform_add_group β]
[topological_ring β]
(f : α →+* β) :
The completion map as a ring morphism.
@[instance]
def
uniform_space.completion.comm_ring
(R : Type u_2)
[comm_ring R]
[uniform_space R]
[uniform_add_group R]
[topological_ring R] :
Equations
- uniform_space.completion.comm_ring R = {add := ring.add uniform_space.completion.ring, add_assoc := _, zero := ring.zero uniform_space.completion.ring, zero_add := _, add_zero := _, neg := ring.neg uniform_space.completion.ring, add_left_neg := _, add_comm := _, mul := ring.mul uniform_space.completion.ring, mul_assoc := _, one := ring.one uniform_space.completion.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
theorem
uniform_space.ring_sep_rel
(α : Type u_1)
[comm_ring α]
[uniform_space α]
[uniform_add_group α]
[topological_ring α] :
theorem
uniform_space.ring_sep_quot
(α : Type u_1)
[r : comm_ring α]
[uniform_space α]
[uniform_add_group α]
[topological_ring α] :
def
uniform_space.sep_quot_equiv_ring_quot
(α : Type u_1)
[r : comm_ring α]
[uniform_space α]
[uniform_add_group α]
[topological_ring α] :
Equations
@[instance]
def
uniform_space.comm_ring
{α : Type u_1}
[comm_ring α]
[uniform_space α]
[uniform_add_group α]
[topological_ring α] :
Equations
- uniform_space.comm_ring = uniform_space.comm_ring._proof_1.mpr (ideal.quotient.comm_ring ⊥.closure)
@[instance]
def
uniform_space.topological_ring
{α : Type u_1}
[comm_ring α]
[uniform_space α]
[uniform_add_group α]
[topological_ring α] :