OAI/Combinatorics/Progressions/Estimates/NativeEquivalenceTransitivity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.BoolLieFamily line 14
2. instance OAI.Erdos3.BoolLieFamily.instLieRing line 23
3. instance OAI.Erdos3.BoolLieFamily.instLieAlgebra line 28
4. instance OAI.Erdos3.BoolLieFamily.instTopologicalSpace line 38
5. instance OAI.Erdos3.BoolLieFamily.instIsTopologicalAddGroup line 44
6. instance OAI.Erdos3.BoolLieFamily.instContinuousSMul line 50
7. instance OAI.Erdos3.BoolLieFamily.instT2Space line 56
8. def OAI.Erdos3.NativeNilsequenceExpansion.ofFamily line 76
9. def OAI.Erdos3.NativeNilsequenceExpansion.weightedSum line 101
10. theorem OAI.Erdos3.NativeVectorEquivalence.mono line 141
11. theorem OAI.Erdos3.NativeVectorEquivalence.symm line 149
12. theorem OAI.Erdos3.NativeVectorEquivalence.conjugate line 159
13. def OAI.Erdos3.NativeNilsequenceExpansion.ofProduct line 183
14. def OAI.Erdos3.NativeNilsequenceExpansion.mul line 235
15. theorem OAI.Erdos3.NativeVectorEquivalence.trans line 278
16. theorem OAI.Erdos3.NativeVectorEquivalence.exists_trans_budget line 316