OAI/Combinatorics/SquareDifference/ResidueReindex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SquareDifference.residueReindex line 21
2. lemma OAI.SquareDifference.residueReindex_neg line 25
3. lemma OAI.SquareDifference.residueReindex_natCast line 41
4. lemma OAI.SquareDifference.prodChar_reindex line 57
5. lemma OAI.SquareDifference.supportDenominator_reindex line 73
6. lemma OAI.SquareDifference.residueFourier_reindex line 90
7. lemma OAI.SquareDifference.squareMultiplier_reindex line 98
8. lemma OAI.SquareDifference.sequenceResidueFourier_reindex line 116
9. lemma OAI.SquareDifference.low_pair_reindex line 125