OAI/NumberTheory/DirichletL/Hecke/DetectorDynamicSelection.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.HeckeDetectorDynamicSelection.actual_witness_familyline 10 - def
OAI.SevenEighths.HeckeDetectorDynamicSelection.fiberline 30 - theorem
OAI.SevenEighths.HeckeDetectorDynamicSelection.card_eq_sum_fibersline 36