commRingTopologicalClosure — Mathlib

English

If a subalgebra s is commutative, its topological closure is a commutative ring.

Русский

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

LaTeX

$$CommRing (s.topologicalClosure)$$

Lean4

/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.
See note [reducible non-instances]. -/
abbrev commRingTopologicalClosure [T2Space A] (s : Subalgebra R A) (hs : ∀ x y : s, x * y = y * x) :
    CommRing s.topologicalClosure :=
  { s.topologicalClosure.toRing, s.toSubmonoid.commMonoidTopologicalClosure hs with }

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