lpSpace

📁 Source: Mathlib/Analysis/CStarAlgebra/lpSpace.lean

Statistics

Metric	Count
Definitions instCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial, instNonUnitalCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal, instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal, instNormedRingSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial	4
Theorems	0
Total	4

(root)

Definitions

Name	Category	Theorems
instCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial 📖	CompOp	—
instNonUnitalCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal 📖	CompOp	—
instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal 📖	CompOp	—
instNormedRingSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial 📖	CompOp	—

---

← Back to Index