OAI/NumberTheory/DirichletL/PrimeRows/Euler.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeHighRowFamily.targetRow line 11
2. theorem OAI.SevenEighths.ProbeHighRowFamily.rowCharacter_hasProd line 13
3. theorem OAI.SevenEighths.ProbeHighRowFamily.targetRow_hasProd line 24
4. def OAI.SevenEighths.ProbeHighRowFamily.localCorrection line 34
5. def OAI.SevenEighths.ProbeHighRowFamily.globalCorrection line 40
6. theorem OAI.SevenEighths.ProbeHighRowFamily.localCorrection_hasProd line 43
7. theorem OAI.SevenEighths.ProbeHighRowFamily.globalCorrection_multipliable line 62
8. theorem OAI.SevenEighths.ProbeHighRowFamily.high_L_factorization line 68