instCommSemiringSubtypeMemSubalgebraOfT2Space

English

If a subalgebra s of A is commutative, then its topological closure s.topologicalClosure carries a commutative ring structure.

Русский

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

LaTeX

$$(∀ x y ∈ s, xy = yx) → CommRing(s.topologicalClosure)$$

Lean4

instance [T2Space A] {x : A} : CommSemiring (elemental R x) :=
  commSemiringTopologicalClosure _
    letI : CommSemiring (adjoin R { x }) :=
      adjoinCommSemiringOfComm R fun y hy z hz =>
        by
        rw [mem_singleton_iff] at hy hz
        rw [hy, hz]
    fun _ _ => mul_comm _ _

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