OAI/Analysis/MutuallyUnbiased/TaoCertificate/TargetMerge0.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.targetCombined0_part0 line 9
  2. def OAI.MUB6.TaoCertificate.targetCombined0_part1 line 11
  3. def OAI.MUB6.TaoCertificate.targetCombined0_part2 line 13
  4. def OAI.MUB6.TaoCertificate.targetCombined0 line 15
  5. theorem OAI.MUB6.TaoCertificate.targetCombined0_checked line 17
  6. theorem OAI.MUB6.TaoCertificate.targetCombined0_value line 20