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_reducible]

noncomputable 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_reducible]

noncomputable 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_reducible]

noncomputable 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_reducible]

noncomputable 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.