OAI/Combinatorics/Progressions/Lattices/NativeIntervalResiduePartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.residue_indicator_positiveCyclicNiltest line 12
2. theorem OAI.Erdos3.refine_positive_partition_by_residue line 23
3. theorem OAI.Erdos3.exists_controlled_residue_refinement line 46
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_fixed_observation_residue_partition line 86
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_fixed_shifted_residue_partition line 143
6. theorem OAI.Erdos3.exists_interval_residue_partition line 198