OAI/NumberTheory/DirichletL/Inversion/FirstGlobalParents.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseFirstGlobalParents.ofOriginal line 18
  2. def OAI.SevenEighths.InverseFirstGlobalParents.toOriginal line 25
  3. theorem OAI.SevenEighths.InverseFirstGlobalParents.toOriginal_ofOriginal line 29
  4. theorem OAI.SevenEighths.InverseFirstGlobalParents.toOriginal_fill line 33
  5. theorem OAI.SevenEighths.InverseFirstGlobalParents.ofOriginal_injective line 37
  6. theorem OAI.SevenEighths.InverseFirstGlobalParents.ofOriginal_toOriginal line 41
  7. theorem OAI.SevenEighths.InverseFirstGlobalParents.fill_ofOriginal_injective line 48
  8. def OAI.SevenEighths.InverseFirstGlobalParents.originalOuterSource line 55
  9. theorem OAI.SevenEighths.InverseFirstGlobalParents.originalOuterSource_empty line 58
  10. theorem OAI.SevenEighths.InverseFirstGlobalParents.sum_originalOuterSource line 64
  11. def OAI.SevenEighths.InverseFirstGlobalParents.originalSelector line 69
  12. theorem OAI.SevenEighths.InverseFirstGlobalParents.originalSelector_ofOriginal line 73
  13. theorem OAI.SevenEighths.InverseFirstGlobalParents.originalSelector_ofOriginal_fun line 79
  14. def OAI.SevenEighths.InverseFirstGlobalParents.originalParentSource line 83
  15. theorem OAI.SevenEighths.InverseFirstGlobalParents.mem_originalParentSource line 87
  16. theorem OAI.SevenEighths.InverseFirstGlobalParents.original_fill_valid line 100
  17. theorem OAI.SevenEighths.InverseFirstGlobalParents.originalParentSource_valid line 111
  18. theorem OAI.SevenEighths.InverseFirstGlobalParents.sum_originalParentSource line 118
  19. theorem OAI.SevenEighths.InverseFirstGlobalParents.signed_originalParentSource line 128
  20. theorem OAI.SevenEighths.InverseFirstGlobalParents.real_originalParentSource line 141
  21. theorem OAI.SevenEighths.InverseFirstGlobalParents.original_supports line 154
  22. theorem OAI.SevenEighths.InverseFirstGlobalParents.original_principal_extra line 169
  23. theorem OAI.SevenEighths.InverseFirstGlobalParents.original_parent_data line 179
  24. theorem OAI.SevenEighths.InverseFirstGlobalParents.original_assigned_conditions line 186
  25. theorem OAI.SevenEighths.InverseFirstGlobalParents.original_whole_assigned_conditions line 198
  26. theorem OAI.SevenEighths.InverseFirstGlobalParents.original_priority_slice line 218
  27. theorem OAI.SevenEighths.InverseFirstGlobalParents.original_second_energy_source line 235