OAI/Analysis/Quantum/PPTSquare/OrderedChannel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ChannelCompletion.rename line 11
  2. lemma OAI.ChannelCompletion.rename_cp line 22
  3. lemma OAI.ChannelCompletion.rename_transpose line 27
  4. lemma OAI.ChannelCompletion.rename_ppt line 32
  5. lemma OAI.ChannelCompletion.trace_submatrix_equivalence line 36
  6. lemma OAI.ChannelCompletion.rename_tracePreserving line 39
  7. lemma OAI.ChannelCompletion.rename_comp line 45
  8. lemma OAI.ChannelCompletion.eb_of_rename line 55
  9. def OAI.ExplicitPencil.orderedCoordinates line 70
  10. lemma OAI.ExplicitPencil.orderedCoordinates_first line 73
  11. lemma OAI.ExplicitPencil.orderedCoordinates_second line 75
  12. lemma OAI.ExplicitPencil.orderedCoordinates_flag line 77
  13. def OAI.ExplicitPencil.Theta21 line 79
  14. theorem OAI.ExplicitPencil.main_channel_fin21 line 81