OAI/Combinatorics/SumProduct/Alignment/CorrectedBox02.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CorrectedBoxLeibman.originPolynomial line 17
2. lemma OAI.CorrectedBoxLeibman.originPolynomial_eval line 20
3. lemma OAI.CorrectedBoxLeibman.originPolynomial_coeff line 30
4. theorem OAI.CorrectedBoxLeibman.lineCoefficient_origin line 41
5. lemma OAI.CorrectedBoxLeibman.lineCoefficient_above line 56
6. theorem OAI.CorrectedBoxLeibman.dense_origin_multiplier line 77
7. lemma OAI.CorrectedBoxLeibman.count_finset_image line 145
8. theorem OAI.CorrectedBoxLeibman.dense_basepoint_characters line 161
9. theorem OAI.CorrectedBoxLeibman.box_line_data line 248