OAI/NumberTheory/DirichletL/Hecke/DetectorFinite.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeDetectorFinite.pairSet line 13
2. lemma OAI.SevenEighths.HeckeDetectorFinite.pairCoefficient_zero_left line 16
3. lemma OAI.SevenEighths.HeckeDetectorFinite.pairCoefficient_zero_right line 20
4. theorem OAI.SevenEighths.HeckeDetectorFinite.pairCoefficient_support line 24
5. theorem OAI.SevenEighths.HeckeDetectorFinite.pair_fiber line 53
6. theorem OAI.SevenEighths.HeckeDetectorFinite.terminal_sum_eq_pair_sum line 63
7. def OAI.SevenEighths.HeckeDetectorFinite.dyadicBlock line 80
8. theorem OAI.SevenEighths.HeckeDetectorFinite.terminal_sum_eq_dyadic line 85
9. theorem OAI.SevenEighths.HeckeDetectorFinite.exists_dyadic_block line 102
10. theorem OAI.SevenEighths.HeckeDetectorFinite.nonzero_block_scale_bounds line 115