OAI/NumberTheory/DirichletL/Hecke/DetectorRelativePrime.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeDetectorRelativePrime.idealCoeff_ne_zero_of_coprime line 10
2. theorem OAI.SevenEighths.HeckeDetectorRelativePrime.idealCoeff_inverse line 18
3. theorem OAI.SevenEighths.HeckeDetectorRelativePrime.relative_coefficient_on_ray line 32
4. theorem OAI.SevenEighths.HeckeDetectorRelativePrime.physical_eq_relative_average line 40