OAI/Combinatorics/Progressions/Sampling/NativeGridRightDictionary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.finite_card_real_grid_box line 9

   Distinct definitions of this name: OAI/Combinatorics/Progressions/Sampling/BoundedKernelGridEnumerationBudget.lean:9 (different declaration text). Qualify references as OAI.Erdos3.finite_card_real_grid_box@path.

2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_bounded_native_grid_enumeration line 52
3. structure OAI.Erdos3.RationalFilteredNilmanifold.NativeGridRightDictionary line 113
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeGridRightDictionary.labeling line 133
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_grid_right_dictionary line 153