commSemiringTopologicalClosure — Mathlib

English

If a subsemiring s is commutative under multiplication, then its topological closure is a commutative semiring.

Русский

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

LaTeX

$$CommSemiring (topologicalClosure s) (hs : ∀ x y : s, x y = y x)$$

Lean4

/-- If a subsemiring of a topological semiring is commutative, then so is its
topological closure.

See note [reducible non-instances]. -/
abbrev commSemiringTopologicalClosure [T2Space R] (s : Subsemiring R) (hs : ∀ x y : s, x * y = y * x) :
    CommSemiring s.topologicalClosure :=
  { s.topologicalClosure.toSemiring, s.toSubmonoid.commMonoidTopologicalClosure hs with }

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