OAI/Combinatorics/Progressions/Linear/NativeDilationPairProjections.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.dilationPairProjection line 15
  2. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairProjection_zero line 18
  3. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairProjection_one line 21
  4. def OAI.Erdos3.NilpotentLieFiltration.realDilationPairProjection line 24
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedDilationPairEquiv_projection line 30
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realDilationPairProjection_coord line 42
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realDilationPairProjection_jointly_injective line 48
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realDilationPairProjection_mem line 60
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationPairProjection_lattice line 86
  10. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationSpaceProjection line 95
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationSpaceProjection_mk line 102
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationSpaceProjection_smul line 108
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationSpaceProjection_lipschitz line 115