OAI/NumberTheory/DirichletL/PrimeRows/DetectorBins.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.ProbeHighRowFamily.detector_nonzero_on_buffered_diskline 12 - lemma
OAI.SevenEighths.ProbeHighRowFamily.detectorEntire_nonzero_on_buffered_diskline 30 - lemma
OAI.SevenEighths.ProbeHighRowFamily.exists_detector_buffered_binline 44 - lemma
OAI.SevenEighths.ProbeHighRowFamily.detectorMaximum_eq_nonprincipalline 68