nonUnitalCommRingTopologicalClosure

English

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

Русский

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

LaTeX

$$$s.topologicalClosure\\text{ is a }\\mathrm{NonUnitalCommRing}.$$$

Lean4

/-- If a non-unital star subalgebra of a non-unital topological star algebra is commutative, then
so is its topological closure.

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

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