OAI/NumberTheory/DirichletL/Detector/LocalUnitFrequency.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbePhysical.finite_fourier_unit_scale line 14
  2. theorem OAI.SevenEighths.ProbePhysical.barePhysicalFourier_unit_frequency line 27
  3. theorem OAI.SevenEighths.ProbePhysical.bareCongruenceCoefficient_unit_frequency line 57
  4. lemma OAI.SevenEighths.ProbePhysical.idealRowHom_norm_one_of_coprime line 72
  5. theorem OAI.SevenEighths.ProbePhysical.bareCongruenceCoefficient_unit_frequency_norm line 80
  6. theorem OAI.SevenEighths.ProbePhysical.bareCongruenceCoefficient_unit_frequency_eq_zero_iff line 91
  7. lemma OAI.SevenEighths.ProbePhysical.supported_element_power line 99
  8. lemma OAI.SevenEighths.ProbePhysical.idealRowHom_prime_power_value line 104
  9. lemma OAI.SevenEighths.ProbePhysical.actualSextic_unit_power_ne_zero line 110
  10. theorem OAI.SevenEighths.ProbePhysical.bareCongruenceCoefficient_prime_power_unit_frequency line 117
  11. theorem OAI.SevenEighths.ProbePhysical.bareCongruenceCoefficient_all_prime_powers_unit line 129
  12. theorem OAI.SevenEighths.ProbePhysical.barePhysicalFourier_all_prime_powers_unit line 139
  13. theorem OAI.SevenEighths.ProbePhysical.bareCongruenceCoefficient_all_prime_powers_unit_norm line 151