extensionHom_coe — Mathlib

English

If α is a topological ring, then its completion is a topological ring as well.

Русский

Если α — топологическое кольцо, то его дополнение тоже является топологическим кольцом.

LaTeX

$$$\\text{IsTopologicalRing}(\\mathrm{Completion}(\\alpha))$$$

Lean4

theorem extensionHom_coe [CompleteSpace β] [T0Space β] (a : α) : Completion.extensionHom f hf a = f a := by
  simp only [Completion.extensionHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    UniformSpace.Completion.extension_coe <| uniformContinuous_addMonoidHom_of_continuous hf]

Похожие утверждения