OAI/Combinatorics/Progressions/Linear/DualLieAlgebra.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.DualLieAlgebra line 14
  2. def OAI.Erdos3.dualBaseLinear line 16
  3. def OAI.Erdos3.dualTangentLinear line 20
  4. theorem OAI.Erdos3.dualBaseLinear_tmul line 23
  5. theorem OAI.Erdos3.dualTangentLinear_tmul line 26
  6. def OAI.Erdos3.dualConstantLie line 29
  7. def OAI.Erdos3.dualInfinitesimal line 33
  8. theorem OAI.Erdos3.dualBaseLinear_constant line 36
  9. theorem OAI.Erdos3.dualTangentLinear_constant line 40
  10. theorem OAI.Erdos3.dualBaseLinear_infinitesimal line 44
  11. theorem OAI.Erdos3.dualTangentLinear_infinitesimal line 48
  12. theorem OAI.Erdos3.dualInfinitesimal_injective line 52
  13. theorem OAI.Erdos3.dualLie_decomposition line 56
  14. theorem OAI.Erdos3.ring_zero_lie line 75
  15. theorem OAI.Erdos3.ring_lie_zero line 76
  16. theorem OAI.Erdos3.dualBaseLinear_lie line 78
  17. def OAI.Erdos3.dualBaseLie line 90
  18. theorem OAI.Erdos3.dualInfinitesimal_lie line 94
  19. theorem OAI.Erdos3.dualLie_lowerCentralSeries_eq_bot line 98