Theorems · Theorem · commutative algebra

UniformSpace.Completion.extensionHom_coe

∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f : α →+* β) (hf : Continuous ⇑f) [inst_8 : CompleteSpace β] [inst_9 : T0Space β] (a : α),
  (UniformSpace.Completion.extensionHom f hf) ↑a = f a

Defined in

Mathlib.Topology.Algebra.UniformRing

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingUniformSpaceIsTopologicalRingIsUniformAddGroupUniformSpaceRingIsUniformAddGroupIsTopologicalRingCompleteSpaceT0Space