OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.HasOnlyTrivialInvariantProjections line 15

   Also declared: ComparatorChallenges/IrrationalRotation.lean:322 (same declaration text).

2. def OAI.Invariant233.IsProjectionAtom line 20

   Also declared: ComparatorChallenges/IrrationalRotation.lean:327 (same declaration text).

3. def OAI.Invariant233.IsAtomicVonNeumannAlgebra line 25

   Also declared: ComparatorChallenges/IrrationalRotation.lean:332 (same declaration text).

4. def OAI.Invariant233.IsAbelianVonNeumannAlgebra line 29

   Also declared: ComparatorChallenges/IrrationalRotation.lean:336 (same declaration text).

5. def OAI.Invariant233.IsDiffuseVonNeumannAlgebra line 32

   Also declared: ComparatorChallenges/IrrationalRotation.lean:339 (same declaration text).

6. def OAI.Invariant233.IsFactor line 35

   Also declared: ComparatorChallenges/IrrationalRotation.lean:342 (same declaration text).

7. def OAI.Invariant233.vectorTrace line 40

   Also declared: ComparatorChallenges/IrrationalRotation.lean:347 (same declaration text).

8. def OAI.Invariant233.IsFaithfulTracialVector line 43

   Also declared: ComparatorChallenges/IrrationalRotation.lean:350 (same declaration text).

9. def OAI.Invariant233.IsTypeII1FactorWithVector line 50

   Also declared: ComparatorChallenges/IrrationalRotation.lean:357 (same declaration text).

10. def OAI.Invariant233.HasSeparablePredual line 56

    Also declared: ComparatorChallenges/IrrationalRotation.lean:363 (same declaration text).