OAI/Analysis/KadisonKastler/L2SwapIntertwining.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Extending tensor intertwining identities by density

  1. theorem OAI.KadisonKastler.l2ScalarSwap_intertwines_of_tensor line 16
  2. theorem OAI.KadisonKastler.intertwines_unitary_star line 39