OAI/Analysis/KadisonKastler/RemoteModularCoisometries.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The concrete modular coisometries of the two-ratio product

  1. theorem OAI.KadisonKastler.PointedMatrixSites.exists_modular_scaling_all_vectors line 25
  2. theorem OAI.KadisonKastler.PointedMatrixSites.exists_modular_coisometry_sequence line 59
  3. theorem OAI.KadisonKastler.PointedMatrixSites.exists_modular_graph_shift line 82
  4. theorem OAI.KadisonKastler.PointedMatrixSites.exists_modular_graph_shift_adjoint line 98