ComparatorChallenges/CharacterCriterion.lean

GitHub source file

146 declarations, 1 contain sorry, 0 declared as axioms

1. def OAI.KirchbergRordam.QuotientNormSupport.normedRing line 23

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:23 (same declaration text).

2. abbrev OAI.KirchbergRordam.NormUltrapower.BoundedSeq line 88

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:88 (same declaration text).

3. def OAI.KirchbergRordam.NormUltrapower.normLimit line 90

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:90 (same declaration text).

4. def OAI.KirchbergRordam.NormUltrapower.nullIdeal line 102

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:102 (same declaration text).

5. instance OAI.KirchbergRordam.NormUltrapower.nullIdeal_twoSided line 145

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:145 (same declaration text).

6. instance OAI.KirchbergRordam.NormUltrapower.nullIdeal_closed line 173

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:173 (same declaration text).

7. abbrev OAI.KirchbergRordam.NormUltrapower.Algebra line 210

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:210 (same declaration text).

8. instance OAI.KirchbergRordam.NormUltrapower.quotientNormedRing line 213

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:213 (same declaration text).

9. instance OAI.KirchbergRordam.NormUltrapower.quotientNormedAlgebra line 217

   Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:217 (same declaration text).

10. instance OAI.KirchbergRordam.NormUltrapower.quotientStar line 220

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:220 (same declaration text).

11. instance OAI.KirchbergRordam.NormUltrapower.quotientStarRing line 244

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:244 (same declaration text).

12. instance OAI.KirchbergRordam.NormUltrapower.quotientStarModule line 258

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:258 (same declaration text).

13. def OAI.KirchbergRordam.NormUltrapower.cutRepresentative line 265

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:265 (same declaration text).

14. instance OAI.KirchbergRordam.NormUltrapower.quotientCStarRing line 272

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:272 (same declaration text).

15. instance OAI.KirchbergRordam.NormUltrapower.quotientCStarAlgebra line 370

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:370 (same declaration text).

16. def OAI.KirchbergRordam.NormUltrapower.quotientMap line 372

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:372 (same declaration text).

17. def OAI.KirchbergRordam.NormUltrapower.constantSeq line 376

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:376 (same declaration text).

18. def OAI.KirchbergRordam.NormUltrapower.diagonal line 385

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:385 (same declaration text).

19. def OAI.KirchbergRordam.NormUltrapower.centralSubalgebra line 388

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:388 (same declaration text).

20. instance OAI.KirchbergRordam.NormUltrapower.centralSubalgebra_closed line 391

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:391 (same declaration text).

21. abbrev OAI.KirchbergRordam.NormUltrapower.CentralAlgebra line 395

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:395 (same declaration text).

22. instance OAI.KirchbergRordam.NormUltrapower.centralSubringClass line 398

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:398 (same declaration text).

23. instance OAI.KirchbergRordam.NormUltrapower.centralCStarAlgebra line 402

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:402 (same declaration text).

24. instance OAI.KirchbergRordam.StarCompletion.completionStar line 413

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:413 (same declaration text).

25. instance OAI.KirchbergRordam.StarCompletion.completionContinuousStar line 415

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:415 (same declaration text).

26. instance OAI.KirchbergRordam.StarCompletion.completionStarRing line 418

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:418 (same declaration text).

27. instance OAI.KirchbergRordam.StarCompletion.completionNormedAlgebra line 439

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:439 (same declaration text).

28. instance OAI.KirchbergRordam.StarCompletion.completionStarModule line 442

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:442 (same declaration text).

29. structure OAI.KirchbergRordam.CStarInductiveLimit.System line 464

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:464 (same declaration text).

30. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 475) line 475
31. def OAI.KirchbergRordam.CStarInductiveLimit.Raw line 479

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:479 (same declaration text).

32. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 481) line 481
33. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 483) line 483
34. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 485) line 485
35. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 487) line 487
36. def OAI.KirchbergRordam.CStarInductiveLimit.rawOf line 489

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:489 (same declaration text).

37. def OAI.KirchbergRordam.CStarInductiveLimit.normLift line 493

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:493 (same declaration text).

38. def OAI.KirchbergRordam.CStarInductiveLimit.ringNorm line 496

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:496 (same declaration text).

39. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 538) line 538
40. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 540) line 540
41. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 556) line 556
42. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 571) line 571
43. abbrev OAI.KirchbergRordam.CStarInductiveLimit.Algebra line 587

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:587 (same declaration text).

44. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 589) line 589
45. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 601) line 601
46. structure OAI.KirchbergRordam.CStarInductiveLimit.Chain line 609

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:609 (same declaration text).

47. def OAI.KirchbergRordam.CStarInductiveLimit.Chain.map line 617

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:617 (same declaration text).

48. def OAI.KirchbergRordam.CStarInductiveLimit.Chain.system line 621

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:621 (same declaration text).

49. structure OAI.KirchbergRordam.MaxTensor.CrossSeminorm line 656

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:656 (same declaration text).

50. instance OAI.KirchbergRordam.MaxTensor.(instance at line 662) line 662
51. def OAI.KirchbergRordam.MaxTensor.Raw line 671

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:671 (same declaration text).

52. instance OAI.KirchbergRordam.MaxTensor.(instance at line 673) line 673
53. instance OAI.KirchbergRordam.MaxTensor.(instance at line 675) line 675
54. instance OAI.KirchbergRordam.MaxTensor.(instance at line 677) line 677
55. def OAI.KirchbergRordam.MaxTensor.rawEquiv line 679

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:679 (same declaration text).

56. def OAI.KirchbergRordam.MaxTensor.liftRaw line 684

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:684 (same declaration text).

57. def OAI.KirchbergRordam.MaxTensor.representationSeminorm line 697

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:697 (same declaration text).

58. abbrev OAI.KirchbergRordam.Spatial.Hilbert line 734

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:734 (same declaration text).

59. def OAI.KirchbergRordam.Spatial.map line 737

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:737 (same declaration text).

60. def OAI.KirchbergRordam.Spatial.left line 742

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:742 (same declaration text).

61. def OAI.KirchbergRordam.Spatial.right line 812

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:812 (same declaration text).

62. structure OAI.KirchbergRordam.MinTensor.RepresentationPair line 889

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:889 (same declaration text).

63. def OAI.KirchbergRordam.MinTensor.RepresentationPair.left line 905

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:905 (same declaration text).

64. def OAI.KirchbergRordam.MinTensor.RepresentationPair.right line 909

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:909 (same declaration text).

65. def OAI.KirchbergRordam.MinTensor.RepresentationPair.crossSeminorm line 913

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:913 (same declaration text).

66. def OAI.KirchbergRordam.MinTensor.spatialIndex line 944

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:944 (same declaration text).

67. def OAI.KirchbergRordam.MinTensor.seminorm line 948

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:948 (same declaration text).

68. def OAI.KirchbergRordam.MinTensor.Raw line 966

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:966 (same declaration text).

69. instance OAI.KirchbergRordam.MinTensor.(instance at line 969) line 969
70. instance OAI.KirchbergRordam.MinTensor.(instance at line 972) line 972
71. instance OAI.KirchbergRordam.MinTensor.instStarRingRaw line 974

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:974 (same declaration text).

72. def OAI.KirchbergRordam.MinTensor.rawRingSeminorm line 977

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:977 (same declaration text).

73. instance OAI.KirchbergRordam.MinTensor.(instance at line 1022) line 1022
74. abbrev OAI.KirchbergRordam.MinTensor.Algebra line 1024

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1024 (same declaration text).

75. abbrev OAI.KirchbergRordam.MatrixTensor.Mat line 1032

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1032 (same declaration text).

76. def OAI.KirchbergRordam.MatrixTensor.leftMatrixAlgebra line 1034

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1034 (same declaration text).

77. def OAI.KirchbergRordam.MatrixTensor.rightMatrixAlgebra line 1050

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1050 (same declaration text).

78. def OAI.KirchbergRordam.MatrixTensor.leftMatrix line 1066

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1066 (same declaration text).

79. def OAI.KirchbergRordam.MatrixTensor.rightMatrix line 1070

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1070 (same declaration text).

80. abbrev OAI.KirchbergRordam.PrimeDimensionDrop.Fiber line 1080

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1080 (same declaration text).

81. def OAI.KirchbergRordam.PrimeDimensionDrop.eval line 1082

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1082 (same declaration text).

82. def OAI.KirchbergRordam.PrimeDimensionDrop.subalgebra line 1092

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1092 (same declaration text).

83. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 1096) line 1096
84. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 1099) line 1099
85. abbrev OAI.KirchbergRordam.PrimeDimensionDrop.Algebra line 1109

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1109 (same declaration text).

86. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 1111) line 1111
87. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 1115) line 1115
88. def OAI.KirchbergRordam.UnitaryPaths.phase line 1123

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1123 (same declaration text).

89. def OAI.KirchbergRordam.UnitaryPaths.involutionValue line 1125

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1125 (same declaration text).

90. def OAI.KirchbergRordam.UnitaryPaths.involutionPath line 1128

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1128 (same declaration text).

91. abbrev OAI.KirchbergRordam.MatrixPermutationPath.Mat line 1190

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1190 (same declaration text).

92. def OAI.KirchbergRordam.MatrixPermutationPath.perm line 1192

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1192 (same declaration text).

93. def OAI.KirchbergRordam.MatrixPermutationPath.path line 1202

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1202 (same declaration text).

94. abbrev OAI.KirchbergRordam.MatrixDiagonalPath.Mat line 1233

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1233 (same declaration text).

95. def OAI.KirchbergRordam.MatrixDiagonalPath.block line 1235

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1235 (same declaration text).

96. def OAI.KirchbergRordam.MatrixDiagonalPath.evaluationBlock line 1249

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1249 (same declaration text).

97. def OAI.KirchbergRordam.MatrixDiagonalPath.diagonal line 1259

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1259 (same declaration text).

98. def OAI.KirchbergRordam.MatrixDiagonalPath.interpolate line 1275

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1275 (same declaration text).

99. def OAI.KirchbergRordam.MatrixBlockReindex.sumBlock line 1291

    Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1291 (same declaration text).

100. def OAI.KirchbergRordam.BalancedDropSystem.cardEquiv line 1326

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1326 (same declaration text).

101. def OAI.KirchbergRordam.BalancedDropSystem.half line 1330

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1330 (same declaration text).

102. def OAI.KirchbergRordam.BalancedDropSystem.lowerPath line 1338

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1338 (same declaration text).

103. def OAI.KirchbergRordam.BalancedDropSystem.upperPath line 1347

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1347 (same declaration text).

104. def OAI.KirchbergRordam.GeneralBlockReindex.repackLeft line 1367

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1367 (same declaration text).

105. def OAI.KirchbergRordam.GeneralBlockReindex.repackRight line 1378

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1378 (same declaration text).

106. structure OAI.KirchbergRordam.GeneralDropSystem.Data line 1449

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1449 (same declaration text).

107. abbrev OAI.KirchbergRordam.GeneralDropSystem.Low line 1467

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1467 (same declaration text).

108. abbrev OAI.KirchbergRordam.GeneralDropSystem.High line 1469

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1469 (same declaration text).

109. abbrev OAI.KirchbergRordam.GeneralDropSystem.Mid line 1471

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1471 (same declaration text).

110. abbrev OAI.KirchbergRordam.GeneralDropSystem.Slot line 1473

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1473 (same declaration text).

111. abbrev OAI.KirchbergRordam.GeneralDropSystem.Index line 1475

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1475 (same declaration text).

112. abbrev OAI.KirchbergRordam.GeneralDropSystem.ZeroSpace line 1477

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1477 (same declaration text).

113. abbrev OAI.KirchbergRordam.GeneralDropSystem.OneSpace line 1479

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1479 (same declaration text).

114. def OAI.KirchbergRordam.GeneralDropSystem.zeroLow line 1481

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1481 (same declaration text).

115. def OAI.KirchbergRordam.GeneralDropSystem.zeroMid line 1484

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1484 (same declaration text).

116. def OAI.KirchbergRordam.GeneralDropSystem.zeroOuter line 1487

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1487 (same declaration text).

117. def OAI.KirchbergRordam.GeneralDropSystem.oneLow line 1490

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1490 (same declaration text).

118. def OAI.KirchbergRordam.GeneralDropSystem.oneMid line 1493

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1493 (same declaration text).

119. def OAI.KirchbergRordam.GeneralDropSystem.oneOuter line 1496

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1496 (same declaration text).

120. def OAI.KirchbergRordam.GeneralDropSystem.slotSwap line 1499

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1499 (same declaration text).

121. def OAI.KirchbergRordam.GeneralDropSystem.zeroReindex line 1505

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1505 (same declaration text).

122. def OAI.KirchbergRordam.GeneralDropSystem.oneReindex line 1509

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1509 (same declaration text).

123. def OAI.KirchbergRordam.GeneralDropSystem.eigenpath line 1514

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1514 (same declaration text).

124. def OAI.KirchbergRordam.GeneralDropSystem.interpolatedEvaluation line 1519

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1519 (same declaration text).

125. def OAI.KirchbergRordam.GeneralDropSystem.fiberMap line 1537

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1537 (same declaration text).

126. def OAI.KirchbergRordam.GeneralDropSystem.continuousFamily line 1545

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1545 (same declaration text).

127. def OAI.KirchbergRordam.GeneralDropSystem.rawStep line 1557

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1557 (same declaration text).

128. def OAI.KirchbergRordam.GeneralDropSystem.restrictToSubalgebras line 1595

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1595 (same declaration text).

129. def OAI.KirchbergRordam.GeneralDropSystem.step line 1601

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1601 (same declaration text).

130. structure OAI.KirchbergRordam.PrimeDropPresentation line 1928

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1928 (same declaration text).

131. def OAI.KirchbergRordam.PrimeDropPresentation.Stage line 1939

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1939 (same declaration text).

132. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 1941) line 1941
133. def OAI.KirchbergRordam.PrimeDropPresentation.chain line 1944

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:1944 (same declaration text).

134. abbrev OAI.KirchbergRordam.PrimeDropPresentation.system line 2000

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2000 (same declaration text).

135. def OAI.KirchbergRordam.StandardPrimeMultiplicity.copies line 2007

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2007 (same declaration text).

136. def OAI.KirchbergRordam.StandardPrimeMultiplicity.lower line 2009

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2009 (same declaration text).

137. def OAI.KirchbergRordam.StandardPrimeMultiplicity.upper line 2011

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2011 (same declaration text).

138. def OAI.KirchbergRordam.StandardPrimeMultiplicity.middle line 2013

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2013 (same declaration text).

139. def OAI.KirchbergRordam.StandardPrimeMultiplicity.next line 2015

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2015 (same declaration text).

140. def OAI.KirchbergRordam.StandardPrimeMultiplicity.data line 2017

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2017 (same declaration text).

141. def OAI.KirchbergRordam.StandardPrimeMultiplicity.size line 2070

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2070 (same declaration text).

142. def OAI.KirchbergRordam.StandardPrimeModel.presentation line 2078

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2078 (same declaration text).

143. def OAI.KirchbergRordam.JiangSu.Algebra line 2116

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2116 (same declaration text).

144. instance OAI.KirchbergRordam.JiangSu.(instance at line 2118) line 2118
145. def OAI.KirchbergRordam.HasNoCharacters line 2125

     Also declared: OAI/Analysis/CharacterCriterion/Definitions.lean:2125 (same declaration text).

146. theorem OAI.KirchbergRordam.character_criterion Challenge statement: The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability sorry line 2128

     L4DEL explanation

     The Kirchberg–Rørdam criterion relates Jiang–Su absorption to characters of the central-sequence algebra. The formalized result proves that, for every nonzero unital separable complex $C^*$-algebra $A$ and every free ultrafilter on $\mathbb N$, the norm central-sequence algebra has no nonzero character exactly when $A\cong A\otimes_{\min}\mathcal Z$. No nuclearity, simplicity, trace, or comparison hypothesis is imposed.

     1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
     2. The repository's comparator configuration selects OAI.Analysis.CharacterCriterion.Main as the released solution module checked against this declaration.

     Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

     Distinct definitions of this name: OAI/Analysis/CharacterCriterion/Main.lean:52 (different declaration text). Qualify references as OAI.KirchbergRordam.character_criterion@path.

     theorem character_criterion
         (A : Type) [CStarAlgebra A] [Nontrivial A] [TopologicalSpace.SeparableSpace A]
         (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ)≤Filter.cofinite) :
         OAI.KirchbergRordam.HasNoCharacters (NormUltrapower.CentralAlgebra A ω) ↔
           Nonempty (A ≃⋆ₐ[ℂ] MinTensor.Algebra A JiangSu.Algebra) := by sorry
     …

     Mentions: OAI.KirchbergRordam.HasNoCharacters, OAI.KirchbergRordam.NormUltrapower.CentralAlgebra, OAI.KirchbergRordam.MinTensor.Algebra, OAI.KirchbergRordam.JiangSu.Algebra