OAI/NumberTheory/DirichletL/CubicSieve/Algebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CubicSieve.square_eq_star_of_fourth_eq line 14
  2. theorem OAI.SevenEighths.CubicSieve.cubic_inv_eq_square line 30
  3. theorem OAI.SevenEighths.CubicSieve.cubic_square_eq_star line 36
  4. theorem OAI.SevenEighths.CubicSieve.cubic_fourth_eq line 41
  5. theorem OAI.SevenEighths.CubicSieve.cubic_cube_eq_mask line 48
  6. theorem OAI.SevenEighths.CubicSieve.cubic_row_decomposition line 56
  7. theorem OAI.SevenEighths.CubicSieve.cubic_norm_le_one line 64
  8. theorem OAI.SevenEighths.CubicSieve.row_decomposition_sum line 73
  9. theorem OAI.SevenEighths.CubicSieve.extracted_coefficients_energy_le line 90