OAI/Combinatorics/SumProduct/Alignment/DenseBox01.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DenseBoxComplete.degree_eq_zero line 16
2. lemma OAI.DenseBoxComplete.monomial_bound line 28
3. lemma OAI.DenseBoxComplete.constant_coefficient line 34
4. theorem OAI.DenseBoxComplete.lattice_inverse_all line 80
5. theorem OAI.SquareInduction.finite_dense_choice_general line 129
6. lemma OAI.CorrectedBoxLeibman.dense_large_values line 176
7. theorem OAI.CorrectedBoxLeibman.dense_correlated_lines line 202
8. lemma OAI.LeibmanSquare.iterDiff_affine line 239
9. lemma OAI.LeibmanSquare.polynomial_affine line 252
10. def OAI.LeibmanSquare.integerDirection line 260
11. lemma OAI.LeibmanSquare.polynomial_integer_line line 265