OAI/NumberTheory/DirichletL/GaussSum/ChineseRemainder.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GaussCRT.gauss_sum_chinese_product line 19
  2. def OAI.GaussCRT.leftAddChar line 50
  3. def OAI.GaussCRT.rightAddChar line 63
  4. theorem OAI.GaussCRT.addChar_crt_factor line 76
  5. theorem OAI.GaussCRT.gauss_sum_crt line 91
  6. theorem OAI.GaussCRT.crt_left_axis line 105
  7. theorem OAI.GaussCRT.leftAddChar_std_apply line 126
  8. theorem OAI.GaussCRT.crt_right_axis line 151
  9. theorem OAI.GaussCRT.rightAddChar_std_apply line 172
  10. theorem OAI.GaussCRT.gauss_shift_cross line 197
  11. theorem OAI.GaussCRT.gauss_sum_crt_standard line 223
  12. def OAI.IdealGaussCRT.leftAddChar line 258
  13. def OAI.IdealGaussCRT.rightAddChar line 268
  14. theorem OAI.IdealGaussCRT.addChar_crt_factor line 278
  15. theorem OAI.IdealGaussCRT.gauss_sum_crt line 287
  16. theorem OAI.IdealGaussCRT.gauss_sum_ideal_crt line 311
  17. def OAI.IdealGaussCRT.quotientAddChar line 328
  18. theorem OAI.IdealGaussCRT.quotientAddChar_mk line 347
  19. theorem OAI.IdealGaussCRT.principal_coprime_of_bezout line 352
  20. theorem OAI.IdealGaussCRT.bezout_of_principal_coprime line 360
  21. theorem OAI.IdealGaussCRT.crt_left_inverse_coordinate line 370
  22. theorem OAI.IdealGaussCRT.crt_right_inverse_coordinate line 404
  23. def OAI.IdealGaussCRT.rawTraceChar line 438
  24. theorem OAI.IdealGaussCRT.rawTraceChar_period line 445
  25. def OAI.IdealGaussCRT.traceModChar line 460
  26. theorem OAI.IdealGaussCRT.traceModChar_mk line 468
  27. def OAI.IdealGaussCRT.traceProdChar line 476
  28. theorem OAI.IdealGaussCRT.traceProdChar_mk line 490
  29. theorem OAI.IdealGaussCRT.leftAddChar_traceProd line 498
  30. theorem OAI.IdealGaussCRT.rightAddChar_traceProd line 526
  31. theorem OAI.IdealGaussCRT.bezout_inverse_left line 554
  32. theorem OAI.IdealGaussCRT.bezout_inverse_right line 567
  33. theorem OAI.IdealGaussCRT.gauss_shift_bezout_left line 580
  34. theorem OAI.IdealGaussCRT.gauss_shift_bezout_right line 601
  35. theorem OAI.IdealGaussCRT.gauss_sum_trace_crt line 622
  36. theorem OAI.IdealGaussCRT.gauss_sum_trace_crt_of_coprime line 658