OAI/Combinatorics/Progressions/Linear/AnchoredKernelInvariance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RationalFilteredNilmanifold.refiltered_product_kernel_invariant line 15
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.refiltered_product_pullback_invariant line 35
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.refiltered_top_commutes line 48
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.anchored_kernel_frequency_zero line 77
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.anchored_kernel_observable_invariant line 90
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.anchored_frozen_observable_invariant line 102