OAI/Analysis/CharacterCriterion/SpatialTensor.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KirchbergRordam.GenericRW.Spatial.Hilbert line 25
  2. def OAI.KirchbergRordam.GenericRW.Spatial.map line 28
  3. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_coe line 31
  4. lemma OAI.KirchbergRordam.GenericRW.Spatial.ext line 35
  5. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_add_left line 43
  6. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_add_right line 49
  7. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_smul_left line 55
  8. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_smul_right line 61
  9. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_mul line 67
  10. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_one line 73
  11. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_inner_algebraic line 81
  12. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_inner line 94
  13. lemma OAI.KirchbergRordam.GenericRW.Spatial.map_star line 100
  14. def OAI.KirchbergRordam.GenericRW.Spatial.left line 110
  15. def OAI.KirchbergRordam.GenericRW.Spatial.right line 121
  16. lemma OAI.KirchbergRordam.GenericRW.Spatial.left_right_commute line 132
  17. instance OAI.KirchbergRordam.GenericRW.Spatial.(instance at line 144) line 144
  18. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.nontrivial_of_representations line 152
  19. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 168) line 168
  20. instance OAI.KirchbergRordam.GenericRW.MaxTensor.powerPack_nontrivial line 172
  21. def OAI.KirchbergRordam.GenericRW.MaxTensor.map line 187
  22. def OAI.KirchbergRordam.GenericRW.TripleTensor.firstTwo line 196
  23. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.firstTwo_third line 199
  24. def OAI.KirchbergRordam.GenericRW.TripleTensor.reassociate line 217
  25. theorem OAI.KirchbergRordam.GenericRW.MaxTensor.exists_joinPower line 226
  26. theorem OAI.KirchbergRordam.GenericRW.Fullness.finite_bridges line 246
  27. lemma OAI.KirchbergRordam.GenericRW.Fullness.full_map line 280
  28. lemma OAI.KirchbergRordam.GenericRW.FullSquareZero.orthogonal_of_pair line 293
  29. theorem OAI.KirchbergRordam.GenericRW.FullSquareZero.full_orthogonal_parts line 303
  30. theorem OAI.KirchbergRordam.GenericRW.FullSquareZero.combine_bridges line 314
  31. theorem OAI.KirchbergRordam.GenericRW.FullSquareZero.exists_full_square_zero line 370
  32. theorem OAI.KirchbergRordam.GenericRW.FullSquareZero.normalize line 384