Theorems · Definition · functional analysis

Algebra.elemental

(R : Type u_1) →
  [inst : CommSemiring R] →
    {A : Type u} →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Semiring A] → [inst_3 : Algebra R A] → [IsSemitopologicalSemiring A] → A → Subalgebra R A

The topological closure of the subalgebra generated by a single element.

Defined in

Mathlib.Topology.Algebra.Algebra

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringTopologicalSpaceSemiringAlgebraIsSemitopologicalSemiring