OAI/Combinatorics/SumProduct/Alignment/IntegerArrays13.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.m line 20
2. abbrev OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.h line 21
3. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.perm line 22
4. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.outer line 27
5. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.inner line 29
6. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reconstruct line 33
7. abbrev OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.qdim line 35
8. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.coord line 36
9. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.ownPair line 38
10. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.family line 50
11. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.inside_mem line 66
12. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.outside_notMem line 71
13. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reconstruct_inside line 76
14. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reconstruct_outside line 80
15. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.representative line 84
16. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.representative_data line 86
17. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.ownPair_coord line 108
18. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_frozen_family line 113
19. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.canonical_inner_product line 170
20. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.coprime_of_mod_congr line 182
21. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_residue_congr line 188
22. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_family_numeric line 197