OAI/Analysis/CStarAlgebra/PureInfiniteness/Stabilization.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MainGap.Stable.Mat line 14

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:44 (same declaration text).

2. def OAI.MainGap.Stable.pad line 16

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:46 (same declaration text).

3. lemma OAI.MainGap.Stable.pad_entry line 20

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:50 (same declaration text).

4. lemma OAI.MainGap.Stable.pad_apply line 23

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:53 (same declaration text).

5. lemma OAI.MainGap.Stable.sum_pad line 26

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:56 (same declaration text).

6. lemma OAI.MainGap.Stable.pad_mul line 42

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:72 (same declaration text).

7. def OAI.MainGap.Stable.padHom line 56

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:86 (same declaration text).

8. lemma OAI.MainGap.Stable.pad_injective line 64

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:94 (same declaration text).

9. lemma OAI.MainGap.Stable.norm_pad line 70

   Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:100 (same declaration text).

10. lemma OAI.MainGap.Stable.pad_self line 73

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:103 (same declaration text).

11. lemma OAI.MainGap.Stable.pad_pad line 77

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:107 (same declaration text).

12. instance OAI.MainGap.Stable.pad_directedSystem line 88

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:118 (same declaration text).

13. abbrev OAI.MainGap.Stable.Algebraic line 92

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:122 (same declaration text).

14. instance OAI.MainGap.Stable.(instance at line 100) line 100
15. instance OAI.MainGap.Stable.(instance at line 102) line 102
16. lemma OAI.MainGap.Stable.norm_mk line 105

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:135 (same declaration text).

17. lemma OAI.MainGap.Stable.normedCore line 108

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:138 (same declaration text).

18. instance OAI.MainGap.Stable.(instance at line 125) line 125
19. instance OAI.MainGap.Stable.(instance at line 126) line 126
20. instance OAI.MainGap.Stable.(instance at line 127) line 127
21. instance OAI.MainGap.Stable.(instance at line 132) line 132
22. def OAI.MainGap.Stable.cornerAlg line 137

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:167 (same declaration text).

23. lemma OAI.MainGap.Stable.cornerAlg_apply line 141

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:171 (same declaration text).

24. lemma OAI.MainGap.Stable.cornerAlg_isometry line 144

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:174 (same declaration text).

25. abbrev OAI.MainGap.Stable.Stabilization line 147

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:177 (same declaration text).

26. instance OAI.MainGap.Stable.(instance at line 155) line 155
27. lemma OAI.MainGap.Stable.coe_mul_stable line 159

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:189 (same declaration text).

28. instance OAI.MainGap.Stable.(instance at line 164) line 164
29. instance OAI.MainGap.Stable.(instance at line 172) line 172
30. instance OAI.MainGap.Stable.(instance at line 188) line 188
31. instance OAI.MainGap.Stable.(instance at line 194) line 194
32. lemma OAI.MainGap.Stable.coe_star_stable line 196

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:226 (same declaration text).

33. instance OAI.MainGap.Stable.(instance at line 200) line 200
34. instance OAI.MainGap.Stable.(instance at line 203) line 203
35. instance OAI.MainGap.Stable.(instance at line 215) line 215
36. instance OAI.MainGap.Stable.(instance at line 220) line 220
37. instance OAI.MainGap.Stable.(instance at line 229) line 229
38. instance OAI.MainGap.Stable.(instance at line 238) line 238
39. def OAI.MainGap.Stable.stabilizationCStarAlgebra line 246

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:276 (same declaration text).

40. def OAI.MainGap.Stable.corner line 248

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:278 (same declaration text).

41. lemma OAI.MainGap.Stable.corner_apply line 256

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:286 (same declaration text).

42. lemma OAI.MainGap.Stable.norm_corner line 259

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:289 (same declaration text).

43. lemma OAI.MainGap.Stable.corner_isometry line 262

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:292 (same declaration text).

44. lemma OAI.MainGap.Stable.corner_pad line 265

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:295 (same declaration text).