Theorems · Definition · functional analysis

algebraMapCLM

(R : Type u_1) →
  (A : Type u) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          [inst_3 : TopologicalSpace R] → [inst_4 : TopologicalSpace A] → [ContinuousSMul R A] → R →L[R] A

The inclusion of the base ring in a topological algebra as a continuous linear map.

Defined in

Mathlib.Topology.Algebra.Algebra

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraTopologicalSpaceTopologicalSpaceContinuousSMul