OAI/Combinatorics/Progressions/Lattices/AllocatedWholeResidueShift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_coefficient_entry_bound line 26
2. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_residue_of_principal_label line 47
3. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalResidue_shift_principal line 74
4. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalResidue_offset_shift line 92
5. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_residue_of_whole_label line 155
6. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalResidue_whole_offset_shift line 181