OAI/NumberTheory/DirichletL/FiniteFourier.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.FiniteFourier.IsPrimitiveOnIdeals line 18
  2. theorem OAI.SevenEighths.FiniteFourier.IsPrimitiveOnIdeals.inv line 21
  3. theorem OAI.SevenEighths.FiniteFourier.primitiveOnIdeals_of_field line 30
  4. def OAI.SevenEighths.FiniteFourier.transform line 37
  5. theorem OAI.SevenEighths.FiniteFourier.transform_inversion line 40
  6. theorem OAI.SevenEighths.FiniteFourier.exists_nonzero_annihilator line 62
  7. theorem OAI.SevenEighths.FiniteFourier.exists_unit_stabilizer line 72
  8. theorem OAI.SevenEighths.FiniteFourier.gaussSum_mulShift_nonunit_eq_zero line 88
  9. theorem OAI.SevenEighths.FiniteFourier.primitive_gaussSum_mulShift line 100
  10. theorem OAI.SevenEighths.FiniteFourier.transform_primitive_character line 108
  11. theorem OAI.SevenEighths.FiniteFourier.primitive_gaussSum_mul_conjugate line 113
  12. theorem OAI.SevenEighths.FiniteFourier.primitive_gaussSum_norm_sq line 130
  13. theorem OAI.SevenEighths.FiniteFourier.primitive_gaussSum_norm line 138
  14. theorem OAI.SevenEighths.FiniteFourier.primitive_gaussSum_ne_zero line 143
  15. theorem OAI.SevenEighths.FiniteFourier.primitive_character_expansion line 151