OAI/NumberTheory/DirichletL/Inversion/InitialArithmetic.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialArithmetic.initialColumn line 20
  2. theorem OAI.SevenEighths.InverseInitialArithmetic.initialColumn_eq_secondPre line 27
  3. theorem OAI.SevenEighths.InverseInitialArithmetic.initial_common_extraction line 34
  4. theorem OAI.SevenEighths.InverseInitialArithmetic.initial_marked_child line 44
  5. theorem OAI.SevenEighths.InverseInitialArithmetic.initial_input_row line 57
  6. def OAI.SevenEighths.InverseInitialArithmetic.sourceIdeal line 68
  7. theorem OAI.SevenEighths.InverseInitialArithmetic.sourceIdeal_ne_zero line 72
  8. theorem OAI.SevenEighths.InverseInitialArithmetic.sourceIdeal_union line 76
  9. theorem OAI.SevenEighths.InverseInitialArithmetic.sourceIdeal_gen line 82
  10. theorem OAI.SevenEighths.InverseInitialArithmetic.sourceIdeal_dvd line 94
  11. def OAI.SevenEighths.InverseInitialArithmetic.sourcePrime line 99
  12. def OAI.SevenEighths.InverseInitialArithmetic.sourceTuple line 102
  13. theorem OAI.SevenEighths.InverseInitialArithmetic.source_prime_dvd line 106
  14. theorem OAI.SevenEighths.InverseInitialArithmetic.sourceTuple_valid line 114
  15. theorem OAI.SevenEighths.InverseInitialArithmetic.source_quotient line 132
  16. theorem OAI.SevenEighths.InverseInitialArithmetic.source_child line 142
  17. theorem OAI.SevenEighths.InverseInitialArithmetic.initial_pair_children line 148
  18. theorem OAI.SevenEighths.InverseInitialArithmetic.initial_scalar_self_pair line 167
  19. theorem OAI.SevenEighths.InverseInitialArithmetic.sourceIdeal_injective line 199
  20. structure OAI.SevenEighths.InverseInitialArithmetic.Source line 205
  21. def OAI.SevenEighths.InverseInitialArithmetic.toTuple line 212
  22. theorem OAI.SevenEighths.InverseInitialArithmetic.toTuple_injective line 215
  23. def OAI.SevenEighths.InverseInitialArithmetic.assignedTerm line 232
  24. theorem OAI.SevenEighths.InverseInitialArithmetic.assignedTerm_source line 236
  25. theorem OAI.SevenEighths.InverseInitialArithmetic.actual_source_valid line 246
  26. theorem OAI.SevenEighths.InverseInitialArithmetic.actual_source_fiber_bound line 256
  27. theorem OAI.SevenEighths.InverseInitialArithmetic.poisson_generator_unit line 284
  28. def OAI.SevenEighths.InverseInitialArithmetic.sectorSource line 298
  29. theorem OAI.SevenEighths.InverseInitialArithmetic.sectorSource_injective line 302
  30. theorem OAI.SevenEighths.InverseInitialArithmetic.sectorTuple_injective line 316
  31. theorem OAI.SevenEighths.InverseInitialArithmetic.actual_sector_fiber_bound line 323
  32. theorem OAI.SevenEighths.InverseInitialArithmetic.initial_poisson_child_normalized line 348