lp ∞ A as a C⋆-algebra

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

instance instNonUnitalCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal {I : Type u_1} {A : I → Type u_2} [(i : I) → NonUnitalCStarAlgebra (A i)] : NonUnitalCStarAlgebra ↥(lp A ⊤)

Equations

• instNonUnitalCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal = NonUnitalCStarAlgebra.mk

instance instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal {I : Type u_1} {A : I → Type u_2} [(i : I) → NonUnitalCommCStarAlgebra (A i)] : NonUnitalCommCStarAlgebra ↥(lp A ⊤)

Equations

• instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal = NonUnitalCommCStarAlgebra.mk

instance instNormedRingSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial {I : Type u_1} {A : I → Type u_2} [∀ (i : I), Nontrivial (A i)] [(i : I) → CStarAlgebra (A i)] : NormedRing ↥(lp A ⊤)

Equations

• instNormedRingSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial = NormedRing.mk ⋯ ⋯

instance instCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial {I : Type u_1} {A : I → Type u_2} [∀ (i : I), Nontrivial (A i)] [(i : I) → CommCStarAlgebra (A i)] : CommCStarAlgebra ↥(lp A ⊤)

Equations

• instCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial = CommCStarAlgebra.mk