OAI/NumberTheory/DirichletL/Hecke/DetectorPrimeFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData line 13
2. def OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData.base line 25
3. theorem OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData.base_spec line 29
4. theorem OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData.base_conductor line 35
5. def OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData.character line 40
6. theorem OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData.coefficient_on_ray line 45
7. theorem OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData.amplitude_eq line 55
8. theorem OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData.twisted_conductor line 71
9. theorem OAI.SevenEighths.HeckeDetectorPrimeFamily.RowData.twisted_nonprincipal line 78
10. structure OAI.SevenEighths.HeckeDetectorPrimeFamily.Ramification line 92
11. theorem OAI.SevenEighths.HeckeDetectorPrimeFamily.Ramification.nonprincipal line 112