OAI/Analysis/CharacterCriterion/RepresentedLabels.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.GenericRW.RepresentedLabels.rank_two_of_detecting line 20
  2. lemma OAI.KirchbergRordam.GenericRW.RepresentedLabels.multiply_map line 39
  3. lemma OAI.KirchbergRordam.GenericRW.RepresentedLabels.labels_map_independent line 53
  4. lemma OAI.KirchbergRordam.GenericRW.RepresentedLabels.range_multiply_injective line 61
  5. lemma OAI.KirchbergRordam.GenericRW.RepresentedLabels.independent_multiply_range line 86
  6. theorem OAI.KirchbergRordam.GenericRW.RepresentedLabels.factor_labels line 116
  7. lemma OAI.KirchbergRordam.GenericRW.RepresentedLabels.multiply_selfAdjoint_general line 150
  8. lemma OAI.KirchbergRordam.GenericRW.RepresentedLabels.map_multiply line 166
  9. theorem OAI.KirchbergRordam.GenericRW.RepresentedLabels.power_labels line 180
  10. lemma OAI.KirchbergRordam.GenericRW.GroupedFactors.isFactor_of_three line 225
  11. abbrev OAI.KirchbergRordam.GenericRW.TripleTensor.Algebra line 246
  12. def OAI.KirchbergRordam.GenericRW.TripleTensor.first line 248
  13. def OAI.KirchbergRordam.GenericRW.TripleTensor.second line 249
  14. def OAI.KirchbergRordam.GenericRW.TripleTensor.third line 250
  15. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.first_second line 251
  16. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.first_third line 253
  17. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.second_third line 255
  18. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.commute_of_legs line 259
  19. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.first_factor line 267
  20. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.second_factor line 271
  21. def OAI.KirchbergRordam.GenericRW.TripleTensor.complementSecond line 284
  22. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.complementSecond_commute line 288
  23. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.complementSecond_total line 304
  24. def OAI.KirchbergRordam.GenericRW.TripleTensor.complementThird line 323
  25. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.complementThird_commute line 327
  26. lemma OAI.KirchbergRordam.GenericRW.TripleTensor.complementThird_total line 343