OAI/NumberTheory/DirichletL/RowCompletion/ReflectedFibers.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalRowCompletion.GoodMaskRowData.sum_selectedSourceRowScalar_mul line 81
  2. def OAI.CanonicalRowCompletion.ActualFiber.rowResidue line 109
  3. def OAI.CanonicalRowCompletion.ActualFiber.rowAmplitude line 119
  4. lemma OAI.CanonicalRowCompletion.ActualFiber.rowScalar_eq_ite line 133
  5. theorem OAI.CanonicalRowCompletion.ActualFiber.sum_rowScalar_phase_mul line 142
  6. theorem OAI.CanonicalRowCompletion.ActualFiber.sum_rowScalar_fixedRays line 159
  7. theorem OAI.CanonicalRowCompletion.ActualFiber.sum_rowScalar_fixedRayFin line 176
  8. theorem OAI.CompletedGauss.hasExactCompletedModels_of_representative_identity line 204
  9. def OAI.CanonicalRowCompletion.ActualFiber.sourcePrimeSet line 232
  10. lemma OAI.CanonicalRowCompletion.ActualFiber.sourcePrimeSet_encode line 238
  11. abbrev OAI.CanonicalRowCompletion.ActualFiber.sourceStratum line 245
  12. def OAI.CanonicalRowCompletion.ActualFiber.sourceStratumValue line 254
  13. lemma OAI.CanonicalRowCompletion.ActualFiber.finset_union_image_decidableEq_eq line 275
  14. theorem OAI.CanonicalRowCompletion.ActualFiber.completedT_eq_nonresidual_source line 282
  15. lemma OAI.CompletedGauss.FreeReflection.fixedRayFiber_branch line 375
  16. theorem OAI.CompletedGauss.FreeReflection.fixedRayFiberFromRows_branch_value line 397
  17. lemma OAI.CanonicalRowCompletion.ActualFiber.columnDivisor_ne_zero line 460
  18. theorem OAI.CanonicalRowCompletion.ActualFiber.reflectedFiber_branch_exact line 470
  19. theorem OAI.CanonicalRowCompletion.dirichletTarget_of_reflection_shells line 615
  20. theorem OAI.ShortDraft.zeta_nonvanishing_of_dirichletTarget line 636
  21. def OAI.CanonicalRowCompletion.ActualFiber.sourceDivisor line 653
  22. lemma OAI.CanonicalRowCompletion.ActualFiber.sourceDivisor_ne_zero line 658
  23. def OAI.CanonicalRowCompletion.ActualFiber.sourceCompressedTerm line 666