OAI/Analysis/MutuallyUnbiased/TaoCertificate/TargetMerge1.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.targetCombined1_part0 line 9
  2. def OAI.MUB6.TaoCertificate.targetCombined1_part1 line 11
  3. def OAI.MUB6.TaoCertificate.targetCombined1_part2 line 13
  4. def OAI.MUB6.TaoCertificate.targetCombined1_part3 line 15
  5. def OAI.MUB6.TaoCertificate.targetCombined1 line 17
  6. theorem OAI.MUB6.TaoCertificate.targetCombined1_checked line 19
  7. theorem OAI.MUB6.TaoCertificate.targetCombined1_value line 22