OAI/Analysis/BackwardIntertwiners/OperatorTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Hyperinvariant233.norm_conjugate_le line 13
  2. theorem OAI.Hyperinvariant233.norm_conjugate line 21
  3. theorem OAI.Hyperinvariant233.transitiveCommutant_conjugate line 32
  4. theorem OAI.Hyperinvariant233.mainClaim_transport line 62
  5. theorem OAI.Hyperinvariant233.mem_commutant_iff line 83
  6. theorem OAI.Hyperinvariant233.commutant_isClosed_strong line 93
  7. theorem OAI.Hyperinvariant233.scalar_of_commutant_top line 115
  8. theorem OAI.Hyperinvariant233.commutant_ne_top_of_nonzero_quasinilpotent line 128
  9. theorem OAI.Hyperinvariant233.fullClaim_of_mainClaim line 148