Theorems · Definition · commutative algebra

UniformSpace.Completion.coeRingHom

{α : Type u_1} →
  [inst : Ring α] →
    [inst_1 : UniformSpace α] →
      [inst_2 : IsTopologicalRing α] → [inst_3 : IsUniformAddGroup α] → α →+* UniformSpace.Completion α

The map from a uniform ring to its completion, as a ring homomorphism.

Defined in

Mathlib.Topology.Algebra.UniformRing

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingUniformSpaceIsTopologicalRingIsUniformAddGroup