toAddGroupTopology — Mathlib

English

The forgetful functor from ring topologies to additive group topologies exists, preserving the underlying topological space and the additive group structure.

Русский

Существуют переходы от кольцевых топологий к топологиям аддитивной группы, сохраняющие базовую топологическую структуру.

LaTeX

$$toAddGroupTopology(t) : AddGroupTopology R$$

Lean4

/-- The forgetful functor from ring topologies on `a` to additive group topologies on `a`. -/
def toAddGroupTopology (t : RingTopology R) : AddGroupTopology R
    where
  toTopologicalSpace := t.toTopologicalSpace
  toIsTopologicalAddGroup := @IsTopologicalRing.to_topologicalAddGroup _ _ t.toTopologicalSpace t.toIsTopologicalRing

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