OAI/Combinatorics/Progressions/Lattices/AllocatedCommonResidueMask.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.mixedSiteResidueReduction line 14
2. theorem OAI.Erdos3.VectorPolynomial.mixedSiteResidueReduction_cast line 20
3. def OAI.Erdos3.VectorPolynomial.mixedSiteGridResidue line 28
4. theorem OAI.Erdos3.VectorPolynomial.mixedSiteGridResidue_cast line 32
5. def OAI.Erdos3.VectorPolynomial.allocatedCommonResidueMask line 54
6. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonResidueMask_eval line 60
7. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonResidueMask_norm line 71