OAI/Analysis/JiangSu/TensorProducts/FiniteHilbertAmplification.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PureStateExcision.tupleOp line 17
  2. lemma OAI.PureStateExcision.tupleOp_apply line 23
  3. lemma OAI.PureStateExcision.tupleOp_star line 27
  4. def OAI.PureStateExcision.tupleRepresentation line 33
  5. lemma OAI.PureStateExcision.tupleRepresentation_apply line 48
  6. def OAI.PureStateExcision.tupleSingle line 51
  7. lemma OAI.PureStateExcision.tupleSingle_apply line 56
  8. def OAI.PureStateExcision.tupleEntry line 58
  9. lemma OAI.PureStateExcision.tupleEntry_apply line 63
  10. lemma OAI.PureStateExcision.tupleOp_single line 67
  11. lemma OAI.PureStateExcision.commuting_tuple_entries line 73
  12. lemma OAI.PureStateExcision.tuple_operator_expansion line 86