OAI/Analysis/Kaplansky/StableFiniteness/Definitions.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KaplanskyConsequences.Regular.HilbertSum line 13

   Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:13 (same declaration text).

2. lemma OAI.KaplanskyConsequences.Regular.reindex_mem line 15

   Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:15 (same declaration text).

3. def OAI.KaplanskyConsequences.Regular.reindex line 22

   Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:22 (same declaration text).

4. lemma OAI.KaplanskyConsequences.Regular.reindex_apply line 34

   Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:34 (same declaration text).

5. def OAI.KaplanskyConsequences.Regular.left line 39

   Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:39 (same declaration text).

6. lemma OAI.KaplanskyConsequences.Regular.left_apply line 42

   Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:42 (same declaration text).

7. lemma OAI.KaplanskyConsequences.Regular.left_one line 44

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

8. lemma OAI.KaplanskyConsequences.Regular.left_mul line 45

   Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:45 (same declaration text).

9. lemma OAI.KaplanskyConsequences.Regular.left_star line 51

   Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:51 (same declaration text).

10. def OAI.KaplanskyConsequences.Regular.Algebra line 60

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:60 (same declaration text).

11. instance OAI.KaplanskyConsequences.Regular.(instance at line 63) line 63
12. instance OAI.KaplanskyConsequences.Regular.(instance at line 66) line 66
13. def OAI.KaplanskyConsequences.Regular.generator line 68

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:68 (same declaration text).

14. abbrev OAI.KaplanskyConsequences.Regular.F2 line 77

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:77 (same declaration text).

15. def OAI.KaplanskyConsequences.Regular.diagonal line 85

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:85 (same declaration text).

16. structure OAI.KaplanskyConsequences.ClosedStarIdeal line 98

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:147 (same declaration text).

17. def OAI.KaplanskyConsequences.StablyFinite line 109

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:158 (same declaration text).

18. structure OAI.KaplanskyConsequences.TracialState line 113

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:162 (same declaration text).

19. def OAI.KaplanskyConsequences.TraceFreeStablyFinite line 118

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

20. def OAI.KaplanskyConsequences.Regular.tensorAlgebra line 133

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:182 (same declaration text).

21. instance OAI.KaplanskyConsequences.Regular.instIsClosedContinuousLinearMapComplexIdSubtypePreLpMemAddSubgroupHilbertSumCoeStarSubalgebraTensorAlgebra line 137
22. instance OAI.KaplanskyConsequences.Regular.(instance at line 141) line 141
23. def OAI.KaplanskyConsequences.ReducedQuasitraceLoss line 152

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:200 (same declaration text).

24. def OAI.KaplanskyConsequences.CStarSimple line 169

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:217 (same declaration text).

25. def OAI.KaplanskyConsequences.SimpleStableTensorCounterexample line 174

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:222 (same declaration text).

26. def OAI.KaplanskyConsequences.StableFinitenessBundle line 189

    Also declared: ComparatorChallenges/KaplanskyStableFiniteness.lean:237 (same declaration text).