commRingTopologicalClosure — Mathlib

English

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

Русский

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

LaTeX

$$commRingTopologicalClosure(S)$$

Lean4

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

See note [reducible non-instances]. -/
abbrev commRingTopologicalClosure [T2Space R] (s : Subring R) (hs : ∀ x y : s, x * y = y * x) :
    CommRing s.topologicalClosure :=
  { s.topologicalClosure.toRing, s.toSubmonoid.commMonoidTopologicalClosure hs with }

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