OAI/NumberTheory/DirichletL/Hecke/DetectorBatch.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.HeckeDetectorBatch.Batch line 11
2. abbrev OAI.SevenEighths.HeckeDetectorBatch.Batch.Bin line 38
3. def OAI.SevenEighths.HeckeDetectorBatch.Batch.fiberRows line 41
4. def OAI.SevenEighths.HeckeDetectorBatch.Batch.fiber line 46
5. def OAI.SevenEighths.HeckeDetectorBatch.Batch.q line 53
6. theorem OAI.SevenEighths.HeckeDetectorBatch.Batch.card_eq_sum_fibers line 56
7. theorem OAI.SevenEighths.HeckeDetectorBatch.Batch.card_bound line 63