OAI/Combinatorics/Progressions/Nilpotent/SumNilmanifoldFactors.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.sumLieSpace line 13
2. instance OAI.Erdos3.sumLieRing line 17
3. instance OAI.Erdos3.sumLieAlgebra line 21
4. instance OAI.Erdos3.sumRealificationTopology line 27
5. instance OAI.Erdos3.sumRealificationTopologicalAddGroup line 36
6. instance OAI.Erdos3.sumRealificationContinuousSMul line 46
7. instance OAI.Erdos3.sumRealificationT2Space line 56
8. def OAI.Erdos3.RationalFilteredNilmanifold.sumFactors line 74
9. def OAI.Erdos3.RationalFilteredNilmanifold.sumOrbits line 79