OAI/Combinatorics/Progressions/Estimates/RealifiedMultidegree.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.rationalLieInclusion line 17
  2. theorem OAI.Erdos3.rationalLieInclusion_apply line 22
  3. theorem OAI.Erdos3.rationalLieInclusion_coordinates line 24
  4. theorem OAI.Erdos3.rationalLieInclusion_injective line 28
  5. theorem OAI.Erdos3.realLieBasis_structure line 37
  6. theorem OAI.Erdos3.realification_lowerCentralSeries_eq_bot line 43
  7. def OAI.Erdos3.NilpotentLieBCHGroup.realificationHom line 58
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationHom_coord line 64
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationHom_injective line 67
  10. def OAI.Erdos3.NilpotentLieFiltration.realLayer line 88
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realLayer_antitone line 90
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realLayer_one line 94
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realLayer_terminal line 101
  14. theorem OAI.Erdos3.NilpotentLieFiltration.lie_realLayer_le line 108
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realLayer_lie_mem line 115
  16. def OAI.Erdos3.NilpotentLieFiltration.realification line 119
  17. theorem OAI.Erdos3.NilpotentLieFiltration.rational_inclusion_mem_realLayer line 126
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realificationHom_mem_subgroup line 130
  19. def OAI.Erdos3.MultidegreeLieFiltration.realLayer line 147
  20. theorem OAI.Erdos3.MultidegreeLieFiltration.realLayer_antitone line 149
  21. theorem OAI.Erdos3.MultidegreeLieFiltration.realLayer_zero line 152
  22. theorem OAI.Erdos3.MultidegreeLieFiltration.realLayer_terminal line 159
  23. theorem OAI.Erdos3.MultidegreeLieFiltration.realLayer_lie_mem line 166
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.realLayer_degree_eq line 176
  25. def OAI.Erdos3.MultidegreeLieFiltration.realification line 184