commSemiringTopologicalClosure — Mathlib

English

If a star-subalgebra is commutative, then its topological closure is a commutative subring.

Русский

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

LaTeX

$$If the generating substructure is commutative, then topologicalClosure(s) is a CommRing$$

Lean4

/-- If a star subalgebra of a topological star algebra is commutative, then so is its topological
closure. See note [reducible non-instances]. -/
abbrev commSemiringTopologicalClosure [T2Space A] (s : StarSubalgebra R A) (hs : ∀ x y : s, x * y = y * x) :
    CommSemiring s.topologicalClosure :=
  s.toSubalgebra.commSemiringTopologicalClosure hs

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