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
- One or more equations did not get rendered due to their size.
instance
instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal
{I : Type u_1}
{A : I → Type u_2}
[(i : I) → NonUnitalCommCStarAlgebra (A i)]
:
NonUnitalCommCStarAlgebra ↥(lp A ⊤)
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.