OAI/Combinatorics/Progressions/Estimates/DilationPairFiltration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.dilationPairLayer line 14
  2. theorem OAI.Erdos3.NilpotentLieFiltration.mem_dilationPairLayer line 17
  3. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairLayer_antitone line 21
  4. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairLayer_lie_mem line 35
  5. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairLayer_terminal line 50
  6. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairLayer_top_relation line 58
  7. def OAI.Erdos3.NilpotentLieFiltration.dilationPairSubalgebra line 75
  8. theorem OAI.Erdos3.NilpotentLieFiltration.mem_dilationPairSubalgebra line 80
  9. def OAI.Erdos3.NilpotentLieFiltration.dilationPairFiltration line 85
  10. theorem OAI.Erdos3.NilpotentLieFiltration.mem_dilationPairFiltration_layer line 102
  11. def OAI.Erdos3.NilpotentLieFiltration.dilationPairFirst line 106
  12. def OAI.Erdos3.NilpotentLieFiltration.dilationPairSecond line 109
  13. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPairTop_relation line 112
  14. def OAI.Erdos3.NilpotentLieFiltration.dilationPairLayerEquiv line 117
  15. def OAI.Erdos3.NilpotentLieFiltration.dilationPairFiltrationLayerEquiv line 121