OAI/NumberTheory/DirichletL/Eisenstein/ConstantTermSupport.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.multiset_cube_remainder line 80
  2. lemma OAI.CubicEisenstein.residue_lambda_prime line 96
  3. lemma OAI.CubicEisenstein.constant_coefficient_unramified_count line 100
  4. theorem OAI.CubicEisenstein.constant_coefficient_cube_reduction line 127
  5. lemma OAI.CubicEisenstein.constant_coefficient_ramified_equation line 153
  6. lemma OAI.CubicEisenstein.unit_eq_sign_of_symbol_class line 182
  7. theorem OAI.CubicEisenstein.arithmeticResidueSum_ne_zero_implies_cube line 207
  8. theorem OAI.CubicEisenstein.arithmeticResidueSum_ne_zero_iff_cube line 238
  9. theorem OAI.CubicEisenstein.arithmeticResidueSum_constant_formula line 246
  10. def OAI.CanonicalQuadraticSieve.idealZeroMask line 262
  11. theorem OAI.CanonicalQuadraticSieve.idealSupport_singleton_univ line 265
  12. theorem OAI.CanonicalQuadraticSieve.singleton_rowCoprimeMask_eq_idealZeroMask line 274
  13. theorem OAI.CanonicalQuadraticSieve.canonical_quadraticRow_star line 288
  14. theorem OAI.CanonicalQuadraticSieve.canonical_quadraticRow_squared line 298
  15. def OAI.CanonicalQuadraticSieve.gcdMaskPrimes line 310
  16. instance OAI.CanonicalQuadraticSieve.gcdMaskPrimes_maximal line 314
  17. theorem OAI.CanonicalQuadraticSieve.gcdMaskPrimes_mask line 324
  18. theorem OAI.CanonicalQuadraticSieve.canonical_same_ray_pair_poisson line 356
  19. theorem OAI.CanonicalQuadraticSieve.canonical_pair_unit_invariant line 408
  20. theorem OAI.CanonicalQuadraticSieve.canonical_masked_pair_summable line 447
  21. theorem OAI.CanonicalQuadraticSieve.canonical_pair_lattice_eq_primary_ideal_sum line 466
  22. theorem OAI.CanonicalQuadraticSieve.canonical_mask_lattice_eq_six_all_ideals line 491
  23. theorem OAI.CanonicalQuadraticSieve.badPrime_injective line 539
  24. theorem OAI.CanonicalQuadraticSieve.supported_primaryGenerator_ne_zero line 559
  25. theorem OAI.CanonicalQuadraticSieve.supported_span_primaryGenerator_iff line 563
  26. theorem OAI.CanonicalQuadraticSieve.badPrime_mask_primaryGenerator line 576
  27. theorem OAI.CanonicalQuadraticSieve.canonical_supported_lattice_eq_six_ideals line 580
  28. theorem OAI.CanonicalQuadraticSieve.canonical_supported_pair_poisson line 599