OAI/Combinatorics/SquareDifference/PositiveResidue.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.exists_strict_square_steps line 13
2. lemma OAI.SquareDifference.prefix_cyclic_difference line 46
3. lemma OAI.SquareDifference.exists_cyclic_labels line 62
4. lemma OAI.SquareDifference.exists_product_strict_steps line 75
5. lemma OAI.SquareDifference.exists_good_cyclic_labels line 98
6. lemma OAI.SquareDifference.tupleCycle_order line 113
7. lemma OAI.SquareDifference.cycleVertex_fin_injective line 119
8. lemma OAI.SquareDifference.cycleVertex_fin_successor line 127
9. lemma OAI.SquareDifference.exists_good_tuple_residues line 139
10. lemma OAI.SquareDifference.uniform_event_positive line 149