OAI/NumberTheory/DirichletL/Detector/HighRowsSelectedUnramified.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.ProbeEuler.unramifiedSelectedline 9 - lemma
OAI.SevenEighths.ProbeEuler.selected_phase_identitiesline 13 - lemma
OAI.SevenEighths.ProbeEuler.unramifiedSelected_error_boundline 26 - lemma
OAI.SevenEighths.ProbeEuler.unramifiedSelected_boundline 50 - lemma
OAI.SevenEighths.ProbeEuler.unramifiedSelected_zeroline 69 - lemma
OAI.SevenEighths.ProbeEuler.unramifiedSelected_zero_boundline 76