OAI/Analysis/IrrationalRotation/Operators/JointEigenprojection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.mem_jointEigenspace line 15
  2. theorem OAI.Invariant233.map_mem_jointEigenspace line 21
  3. theorem OAI.Invariant233.commute_starProjection_of_reducing line 30
  4. theorem OAI.Invariant233.isStarProjection_jointEigenprojection line 47
  5. theorem OAI.Invariant233.jointEigenprojection_mem_generated line 51
  6. theorem OAI.Invariant233.jointEigenprojection_mem_commutant line 63
  7. theorem OAI.Invariant233.exists_mul_jointEigenprojection_ne_zero line 78
  8. theorem OAI.Invariant233.atomic_generated_of_jointEigenprojection_atoms line 99