OAI/Combinatorics/SquareDifference/CyclicIndicator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.sum_zmod_val line 15
2. lemma OAI.SquareDifference.sum_zmod_val_support line 25
3. def OAI.SquareDifference.selectedIndicator line 36
4. lemma OAI.SquareDifference.selectedIndicator_bound line 40
5. lemma OAI.SquareDifference.selectedIndicator_zero line 49
6. lemma OAI.SquareDifference.selectedIndicator_mem line 59
7. lemma OAI.SquareDifference.selectedIndicator_norm line 69
8. lemma OAI.SquareDifference.selectedIndicator_order line 82
9. lemma OAI.SquareDifference.selectedIndicator_square line 91