OAI/NumberTheory/SiegelZeros/Selection/PivotReindexing.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.sum_equiv_finset line 13
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.card_equiv_finset line 20
3. def OAI.SiegelZeros.SiegelZerosAwei.W31.pivotFirstSum line 24
4. def OAI.SiegelZeros.SiegelZerosAwei.W31.pivotOtherSum line 26
5. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.reindexed_first_sum line 28
6. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.reindexed_other_sum line 33
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.reindexed_first_sum_real line 38
8. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.reindexed_other_sum_real line 43
9. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.reindexed_first_fiber_card line 49
10. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.reindexed_cutoff_iff line 57
11. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.sum_equiv_coordinate_image line 66
12. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.card_equiv_coordinate_image line 74
13. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.exists_selected_det_with_exact_sums line 81
14. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ordered_sum_finset line 94
15. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ordered_coordinate_image_sum line 100
16. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ordered_coordinate_pivot_data line 107
17. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ordered_coordinate_fiber_card line 121
18. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ordered_total_order_sum line 131
19. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ordered_total_order_image_sum line 143