OAI/NumberTheory/DirichletL/PrimeRows/TargetPrincipal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeHighRowFamily.targetPrincipalSupport line 13
2. lemma OAI.SevenEighths.ProbeHighRowFamily.targetPrincipalSupport_prime line 16
3. lemma OAI.SevenEighths.ProbeHighRowFamily.inverse_target_elementCoeff line 20
4. theorem OAI.SevenEighths.ProbeHighRowFamily.principal_target_row_norm_bound line 34
5. theorem OAI.SevenEighths.ProbeHighRowFamily.excluded_target_nonprincipal_eventually line 59