commRingTopologicalClosure — Mathlib

English

If the underlying subalgebra is commutative, then the closure as a ring is commutative.

Русский

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

LaTeX

$$If $s$ is commutative then $s.topologicalClosure$ is commutative as a ring$$

Lean4

/-- If a star subalgebra of a topological star algebra is commutative, then so is its topological
closure. See note [reducible non-instances]. -/
abbrev commRingTopologicalClosure {R A} [CommRing R] [StarRing R] [TopologicalSpace A] [Ring A] [Algebra R A]
    [StarRing A] [StarModule R A] [IsTopologicalRing A] [ContinuousStar A] [T2Space A] (s : StarSubalgebra R A)
    (hs : ∀ x y : s, x * y = y * x) : CommRing s.topologicalClosure :=
  s.toSubalgebra.commRingTopologicalClosure hs

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