OAI/Analysis/Commutator/FreeCovariance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.FreeBlocks.factorBounded line 43
  2. lemma OAI.Kadison.FreeBlocks.factorBounded_surjective line 46
  3. lemma OAI.Kadison.FreeBlocks.factorBounded_value line 52
  4. lemma OAI.Kadison.FreeBlocks.factorBounded_GNS line 55
  5. def OAI.Kadison.FreeBlocks.levelWord line 61
  6. lemma OAI.Kadison.FreeBlocks.sourceLevelShuffle_bounded line 71
  7. def OAI.Kadison.FreeBlocks.endpointCoordinate line 83
  8. lemma OAI.Kadison.FreeBlocks.endpointCoordinate_pure line 87
  9. lemma OAI.Kadison.FreeBlocks.sourceLevel_ext line 95
  10. lemma OAI.Kadison.FreeBlocks.sourceLevelEmbedding_word line 130
  11. def OAI.Kadison.FreeBlocks.sourceLeft line 139
  12. lemma OAI.Kadison.FreeBlocks.sourceLeft_word line 145
  13. lemma OAI.Kadison.FreeBlocks.sourceLevelEmbedding_left line 152