OAI/NumberTheory/DirichletL/Detector/CompletedCRTPhase.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.ProbePhase.reciprocitySign_starline 11 - theorem
OAI.SevenEighths.ProbePhase.completed_cubic_pair_cancelline 14 - lemma
OAI.SevenEighths.ProbePhase.sexticPair_mul_leftline 33 - lemma
OAI.SevenEighths.ProbePhase.sexticPair_mul_rightline 39 - lemma
OAI.SevenEighths.ProbePhase.sexticPair_cube_leftline 45 - lemma
OAI.SevenEighths.ProbePhase.sexticPair_cube_rightline 49 - theorem
OAI.SevenEighths.ProbePhase.sexticPair_cube_supportedline 53 - theorem
OAI.SevenEighths.ProbePhase.completed_cubic_cross_cancelline 72