OAI/Combinatorics/Progressions/Probability/RefinedSliceLaws.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteCubeSlice.retained_refineResidues_total_pos line 13
2. theorem OAI.Erdos3.FiniteCubeSlice.refineResidues_complexMean line 22
3. theorem OAI.Erdos3.FiniteCubeSlice.residueLabelMap_coordinate_mod line 37
4. theorem OAI.Erdos3.FiniteCoefficientSlice.retained_refineResidues_total_pos line 49
5. theorem OAI.Erdos3.FiniteCoefficientSlice.refineResidues_complexMean line 57