OAI/Combinatorics/Progressions/Nilpotent/NativeNilsequenceExpansion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.conjugate line 16
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_conjugate line 28
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.conjugate_complexityLE line 31
4. structure OAI.Erdos3.NativeNilsequenceExpansion line 44
5. def OAI.Erdos3.NativeNilsequenceExpansion.mono line 70
6. def OAI.Erdos3.NativeNilsequenceExpansion.conjugate line 77
7. structure OAI.Erdos3.NativeVectorEquivalence line 92