nonUnitalCommSemiringTopologicalClosure

English

If a non-unital subalgebra is commutative, its topological closure is a commutative non-unital semiring.

Русский

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

LaTeX

$$NonUnitalCommSemiring (s.topologicalClosure)$$

Lean4

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

See note [reducible non-instances]. -/
abbrev nonUnitalCommSemiringTopologicalClosure [T2Space A] (s : NonUnitalSubalgebra R A)
    (hs : ∀ x y : s, x * y = y * x) : NonUnitalCommSemiring s.topologicalClosure :=
  s.toNonUnitalSubsemiring.nonUnitalCommSemiringTopologicalClosure hs

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