OAI/NumberTheory/DirichletL/ChineseRemainder/PrimaryCompletions.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ShortDraftCRT.primary_coprime_nine line 83
  2. lemma OAI.ShortDraftCRT.nine_coprime_of_not_lambda_dvd line 87
  3. lemma OAI.ShortDraftCRT.primary_numerator_controlled_inverse line 94
  4. lemma OAI.ShortDraftCRT.completion_primary_lower_right line 99
  5. lemma OAI.ShortDraftCRT.completion_negative_upper_right line 106
  6. theorem OAI.ShortDraftCRT.exists_primary_numerator_completion line 113
  7. theorem OAI.ShortDraftCRT.exists_unramified_denominator_completion line 127
  8. theorem OAI.ShortDraftCRT.exists_primary_denominator_completion line 138
  9. lemma OAI.ShortDraftCRT.controlled_inverse_sector line 164
  10. theorem OAI.ShortDraftCRT.exists_fixed_matrix_completion_controlled line 169
  11. def OAI.ShortDraftCRT.controlledCompletionMatrix line 196
  12. theorem OAI.ShortDraftCRT.exists_primary_numerator_matrix line 199
  13. theorem OAI.ShortDraftCRT.exists_primary_denominator_matrix line 212
  14. lemma OAI.ShortDraftCRT.controlled_primary_principal line 225
  15. lemma OAI.ShortDraftCRT.controlled_primary_ramified line 233
  16. lemma OAI.ShortDraftCRT.controlled_denominator_unramified line 241
  17. theorem OAI.ShortDraftCRT.exists_primary_numerator_sector_completions line 252
  18. theorem OAI.ShortDraftCRT.exists_primary_denominator_sector_completions line 291
  19. theorem OAI.CubicEisenstein.sum_smoothedKernel_common_cusp line 338
  20. def OAI.CanonicalRowCompletion.coprimalityMask line 392
  21. lemma OAI.CanonicalRowCompletion.coprimalityMask_norm line 399
  22. lemma OAI.CanonicalRowCompletion.isCoprime_congr_mod line 403
  23. lemma OAI.CanonicalRowCompletion.coprimalityMask_periodic line 413
  24. lemma OAI.CanonicalRowCompletion.idealRowHom_prime_sixth_mask line 419
  25. theorem OAI.CanonicalRowCompletion.idealRowHom_sixth_mask line 427
  26. lemma OAI.CanonicalRowCompletion.idealRowHom_sixth_eq_mask line 448
  27. lemma OAI.CanonicalRowCompletion.rowTwist_extract_sixth_mask line 454
  28. theorem OAI.ShortDraftCusp.embedded_symbol_product line 474
  29. theorem OAI.ShortDraftCusp.conjugate_symbol_product line 483
  30. theorem OAI.ShortDraftCusp.conjugate_symbol_product_frequency line 494
  31. lemma OAI.ShortDraftCusp.A4_field_inverse line 510
  32. lemma OAI.ShortDraftCusp.A4_active_local line 534
  33. lemma OAI.ShortDraftCusp.A4_complement_inverse line 556