OAI/NumberTheory/DirichletL/Dictionary/InverseMarkedReferenceTuples.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.Tuple line 13
2. abbrev OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.Assigned line 14
3. abbrev OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.Remaining line 15
4. def OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.joinTuple line 17
5. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.sum_tuple_split line 20
6. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.sum_tuple_original line 25
7. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.tuple_injective line 41
8. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.original_selected_subset_sum line 49
9. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.original_selected_grouped line 66