OAI/NumberTheory/DirichletL/CubicSieve/ClosedRecursion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SecondPassArithmetic.two_windows_bound line 85
2. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_state_step line 96
3. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_polynomial_step line 229
4. theorem OAI.SecondPassArithmetic.reopenedCanonicalFirstErrors_power line 321
5. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_closed_step line 414
6. theorem OAI.CompletedGauss.nonresidual_count_eq_on_fiber line 486
7. theorem OAI.CompletedGauss.nonresidual_prime_transport line 514
8. lemma OAI.CompletedGauss.completedResidualScale_eq_on_fiber line 539
9. lemma OAI.CubicEisenstein.compact_estimate_prod_antilipschitz line 557
10. lemma OAI.CubicEisenstein.finiteDimensional_ker_of_compact_estimate line 580
11. lemma OAI.CubicEisenstein.antilipschitz_of_injective_compact_estimate line 599