OAI/NumberTheory/DirichletL/PrimeRows/Agreement.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeHighRowFamily.ramifiedIndices line 11
2. theorem OAI.SevenEighths.ProbeHighRowFamily.mem_ramifiedIndices line 14
3. def OAI.SevenEighths.ProbeHighRowFamily.ramifiedFactor line 22
4. theorem OAI.SevenEighths.ProbeHighRowFamily.ramifiedFactor_hasProd line 27
5. theorem OAI.SevenEighths.ProbeHighRowFamily.supported_prime_coprime line 49
6. theorem OAI.SevenEighths.ProbeHighRowFamily.continuedCorrection_eq_initial line 62
7. theorem OAI.SevenEighths.ProbeHighRowFamily.high_L_factorization_continued line 85