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 ⋯ ⋯