OAI/Combinatorics/SquareDifference/GateExpansion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SquareDifference.OtherVertices line 15
2. instance OAI.SquareDifference.(instance at line 17) line 17
3. instance OAI.SquareDifference.(instance at line 19) line 19
4. lemma OAI.SquareDifference.product_pair_split line 21
5. lemma OAI.SquareDifference.otherVertices_card line 29
6. lemma OAI.SquareDifference.multilinear_pair_expand line 43
7. lemma OAI.SquareDifference.primeProduct_union_le line 71
8. lemma OAI.SquareDifference.primeProduct_biUnion_le line 78
9. lemma OAI.SquareDifference.intervalPiece_depends line 88
10. lemma OAI.SquareDifference.interval_piece_product_bound line 106