OAI/Analysis/JiangSu/CuntzSemigroup/FiniteCuntzOrthogonal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Pureness.positiveSqrt line 15

   Also declared: OAI/Analysis/JiangSu/DimensionFunctions/FiniteSpectralIntegralOrthogonal.lean:38 (same declaration text).

2. theorem OAI.Pureness.positiveSqrt_star line 17

   Also declared: OAI/Analysis/JiangSu/DimensionFunctions/FiniteSpectralIntegralOrthogonal.lean:40 (same declaration text).

3. theorem OAI.Pureness.positiveSqrt_mul line 20

   Also declared: OAI/Analysis/JiangSu/DimensionFunctions/FiniteSpectralIntegralOrthogonal.lean:43 (same declaration text).

4. lemma OAI.Pureness.finitePositiveClass_polar line 25
5. theorem OAI.Pureness.finitePositiveClass_orthogonal_add line 31