C⋆-algebras of continuous functions

We place these here because, for reasons related to the import hierarchy, they cannot be placed in earlier files.

instance BoundedContinuousFunction.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCStarAlgebra A] : NonUnitalCStarAlgebra (BoundedContinuousFunction α A)

Equations

• BoundedContinuousFunction.instNonUnitalCStarAlgebra = NonUnitalCStarAlgebra.mk

instance BoundedContinuousFunction.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCommCStarAlgebra A] : NonUnitalCommCStarAlgebra (BoundedContinuousFunction α A)

Equations

• BoundedContinuousFunction.instNonUnitalCommCStarAlgebra = NonUnitalCommCStarAlgebra.mk

instance BoundedContinuousFunction.instCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CStarAlgebra A] : CStarAlgebra (BoundedContinuousFunction α A)

Equations

• BoundedContinuousFunction.instCStarAlgebra = CStarAlgebra.mk

instance BoundedContinuousFunction.instCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CommCStarAlgebra A] : CommCStarAlgebra (BoundedContinuousFunction α A)

Equations

• BoundedContinuousFunction.instCommCStarAlgebra = CommCStarAlgebra.mk

instance ContinuousMap.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [NonUnitalCStarAlgebra A] : NonUnitalCStarAlgebra C(α, A)

Equations

• ContinuousMap.instNonUnitalCStarAlgebra = NonUnitalCStarAlgebra.mk

instance ContinuousMap.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [NonUnitalCommCStarAlgebra A] : NonUnitalCommCStarAlgebra C(α, A)

Equations

• ContinuousMap.instNonUnitalCommCStarAlgebra = NonUnitalCommCStarAlgebra.mk

instance ContinuousMap.instCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [CStarAlgebra A] : CStarAlgebra C(α, A)

Equations

• ContinuousMap.instCStarAlgebra = CStarAlgebra.mk

instance ContinuousMap.instCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [CommCStarAlgebra A] : CommCStarAlgebra C(α, A)

Equations

• ContinuousMap.instCommCStarAlgebra = CommCStarAlgebra.mk

instance ZeroAtInftyContinuousMap.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCStarAlgebra A] : NonUnitalCStarAlgebra (ZeroAtInftyContinuousMap α A)

Equations

• ZeroAtInftyContinuousMap.instNonUnitalCStarAlgebra = NonUnitalCStarAlgebra.mk

instance ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCommCStarAlgebra A] : NonUnitalCommCStarAlgebra (ZeroAtInftyContinuousMap α A)

Equations

• ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra = NonUnitalCommCStarAlgebra.mk