Theorems · Definition · functional analysis

Subalgebra.commRingTopologicalClosure

{R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u} →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Ring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : IsSemitopologicalRing A] →
              [T2Space A] → (s : Subalgebra R A) → (∀ (x y : ↥s), x * y = y * x) → CommRing ↥s.topologicalClosure

If a subalgebra of a topological algebra is commutative, then so is its topological closure. See note [reducible non-instances].

Defined in

Mathlib.Topology.Algebra.Algebra

Cited by

0 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingTopologicalSpaceRingAlgebraIsSemitopologicalRingT2Space