nonUnitalCommRingTopologicalClosure

English

If a nonunital subring S of a topological ring R is commutative, then its topological closure is a commutative nonunital ring.

Русский

Если неполное подкольцо S кольца R коммутативно, то его топологическое замыкание является коммутативным неполным кольцом.

LaTeX

$$NonUnitalCommRing (S_{topologicalClosure})$$

Lean4

/-- If a non-unital subring of a non-unital topological ring is commutative, then so is its
topological closure.

See note [reducible non-instances] -/
abbrev nonUnitalCommRingTopologicalClosure [T2Space R] (s : NonUnitalSubring R) (hs : ∀ x y : s, x * y = y * x) :
    NonUnitalCommRing s.topologicalClosure :=
  { s.topologicalClosure.toNonUnitalRing, s.toSubsemigroup.commSemigroupTopologicalClosure hs with }

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