OAI/Combinatorics/Progressions/Linear/ModularDesignatedCoefficientRank.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.uniform_expect_coordinate_product line 11
2. theorem OAI.Erdos3.uniform_selected_row_zero_probability_le line 18
3. theorem OAI.Erdos3.designatedPolynomial_linearRow_zero_probability_le line 50
4. theorem OAI.Erdos3.designatedPolynomial_expected_linearRow_zero_le line 72
5. theorem OAI.Erdos3.uniform_expect_unit_scaled_coefficients line 119
6. theorem OAI.Erdos3.designatedPolynomial_expected_unit_linearRow_zero_le line 127
7. theorem OAI.Erdos3.designatedPolynomial_expected_rank_failure_le line 147