OAI/Analysis/CharacterCriterion/ConeCube.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KirchbergRordam.GenericRW.ConeCube.Cube line 27
  2. abbrev OAI.KirchbergRordam.GenericRW.ConeCube.Tensor line 28
  3. abbrev OAI.KirchbergRordam.GenericRW.ConeCube.Fiber line 29
  4. abbrev OAI.KirchbergRordam.GenericRW.ConeCube.Label line 30
  5. def OAI.KirchbergRordam.GenericRW.ConeCube.post line 32
  6. def OAI.KirchbergRordam.GenericRW.ConeCube.first line 42
  7. def OAI.KirchbergRordam.GenericRW.ConeCube.tail line 43
  8. def OAI.KirchbergRordam.GenericRW.ConeCube.matLeg line 45
  9. def OAI.KirchbergRordam.GenericRW.ConeCube.repr line 50
  10. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_left line 59
  11. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_right line 62
  12. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_leg line 65
  13. lemma OAI.KirchbergRordam.GenericRW.ConeCube.scalar_leg_commute line 79
  14. def OAI.KirchbergRordam.GenericRW.ConeCube.scalarLeg line 88
  15. def OAI.KirchbergRordam.GenericRW.ConeCube.κ line 90
  16. lemma OAI.KirchbergRordam.GenericRW.ConeCube.κ_commute line 92
  17. lemma OAI.KirchbergRordam.GenericRW.ConeCube.κ_coordinate line 94
  18. def OAI.KirchbergRordam.GenericRW.ConeCube.point line 98
  19. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_κ line 106
  20. lemma OAI.KirchbergRordam.GenericRW.ConeCube.κ_first line 119
  21. lemma OAI.KirchbergRordam.GenericRW.ConeCube.κ_tail line 121
  22. def OAI.KirchbergRordam.GenericRW.ConeCube.p line 136
  23. def OAI.KirchbergRordam.GenericRW.ConeCube.u line 139
  24. lemma OAI.KirchbergRordam.GenericRW.ConeCube.commuting_gram line 144
  25. lemma OAI.KirchbergRordam.GenericRW.ConeCube.gram_product line 156
  26. lemma OAI.KirchbergRordam.GenericRW.ConeCube.u_gram line 161
  27. lemma OAI.KirchbergRordam.GenericRW.ConeCube.ce_product line 179
  28. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_u line 182
  29. def OAI.KirchbergRordam.GenericRW.ConeCube.expansion line 198
  30. lemma OAI.KirchbergRordam.GenericRW.ConeCube.expansion_zero line 203
  31. lemma OAI.KirchbergRordam.GenericRW.ConeCube.expansion_product line 210
  32. lemma OAI.KirchbergRordam.GenericRW.ConeCube.dense line 235
  33. lemma OAI.KirchbergRordam.GenericRW.ConeCube.faithful line 275
  34. theorem OAI.KirchbergRordam.GenericRW.ConeCube.exists_unique_lift line 281
  35. def OAI.KirchbergRordam.GenericRW.PauliSupport.coord line 295
  36. def OAI.KirchbergRordam.GenericRW.PauliSupport.leg line 299
  37. lemma OAI.KirchbergRordam.GenericRW.PauliSupport.anti_leg line 304
  38. lemma OAI.KirchbergRordam.GenericRW.PauliSupport.coeff_zero line 331
  39. lemma OAI.KirchbergRordam.GenericRW.ConeCube.matLeg_plain line 344
  40. lemma OAI.KirchbergRordam.GenericRW.ConeCube.matLeg_commute line 359
  41. lemma OAI.KirchbergRordam.GenericRW.ConeCube.ccoeff_zero line 374
  42. lemma OAI.KirchbergRordam.GenericRW.ConeCube.p_zero line 383