Theorems · Definition · commutative algebra

UniformSpace.Completion.extensionHom

{α : Type u_1} →
  [inst : Ring α] →
    [inst_1 : UniformSpace α] →
      [inst_2 : IsTopologicalRing α] →
        [inst_3 : IsUniformAddGroup α] →
          {β : Type u} →
            [inst_4 : UniformSpace β] →
              [inst_5 : Ring β] →
                [IsUniformAddGroup β] →
                  [IsTopologicalRing β] →
                    (f : α →+* β) → Continuous ⇑f → [CompleteSpace β] → [T0Space β] → UniformSpace.Completion α →+* β

The completion extension as a ring morphism.

Defined in

Mathlib.Topology.Algebra.UniformRing

Cited by

1 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingUniformSpaceIsTopologicalRingIsUniformAddGroupUniformSpaceRingIsUniformAddGroupIsTopologicalRingCompleteSpaceT0Space