OAI/Analysis/Quantum/PPTSquare/ModularSupport.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ModularSupport.polyVec line 20
  2. lemma OAI.ModularSupport.polyVec_coeff line 21
  3. lemma OAI.ModularSupport.polyVec_degree line 24
  4. lemma OAI.ModularSupport.polyVec_natDegree line 32
  5. lemma OAI.ModularSupport.monic_of_vec line 36
  6. lemma OAI.ModularSupport.natDegree_of_vec line 38
  7. lemma OAI.ModularSupport.powers_of_chain line 42
  8. lemma OAI.ModularSupport.aeval_vec line 54
  9. lemma OAI.ModularSupport.charpoly_of_chain line 60
  10. def OAI.PolynomialCertificate.poly line 114
  11. def OAI.PolynomialCertificate.add line 118
  12. def OAI.PolynomialCertificate.neg line 123
  13. def OAI.PolynomialCertificate.mul line 125
  14. lemma OAI.PolynomialCertificate.poly_map_mul line 129
  15. lemma OAI.PolynomialCertificate.poly_add line 134
  16. lemma OAI.PolynomialCertificate.poly_neg line 142
  17. lemma OAI.PolynomialCertificate.poly_mul line 147
  18. lemma OAI.PolynomialCertificate.poly_eq_zero line 152
  19. lemma OAI.PolynomialCertificate.verify_mul line 159
  20. lemma OAI.PolynomialCertificate.verify_add_mul line 166
  21. lemma OAI.PolynomialCertificate.poly_coeff line 173
  22. lemma OAI.PolynomialCertificate.poly_natDegree_le line 181
  23. lemma OAI.PolynomialCertificate.poly_natDegree_eq line 187
  24. lemma OAI.PolynomialCertificate.verify_sub line 194
  25. lemma OAI.PolynomialCertificate.verify_eq_mul line 200
  26. lemma OAI.PolynomialCertificate.verify_mod line 206
  27. lemma OAI.PolynomialCertificate.mod_trans line 213
  28. lemma OAI.PolynomialCertificate.mod_mul line 215
  29. lemma OAI.PolynomialCertificate.power_mod_mul line 219
  30. lemma OAI.PolynomialCertificate.power_mod_mul_eq line 224
  31. lemma OAI.PolynomialCertificate.gcd_degree_of_mod line 231
  32. def OAI.ModularPencil.N0Num line 255