OAI/Combinatorics/Progressions/Linear/RationalMatrixSeparation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.rational_abs_real_le_numerator line 12
2. theorem OAI.Erdos3.RationalHeightLE.abs_real_le line 19
3. theorem OAI.Erdos3.boundedSpanCell_linear_bound line 25
4. theorem OAI.Erdos3.boundedSpanCell_coordinate_bound line 41
5. theorem OAI.Erdos3.real_matrix_denominator_grid line 59
6. theorem OAI.Erdos3.abs_matrix_mulVec_le line 81
7. theorem OAI.Erdos3.rational_matrix_kernel_separation line 96