OAI/Combinatorics/Progressions/Nilpotent/FreeNilpotentLieAlgebra.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FreeNilpotentLieAlgebra line 11
  2. instance OAI.Erdos3.FreeNilpotentLieAlgebra.instLieRing line 16
  3. instance OAI.Erdos3.FreeNilpotentLieAlgebra.instLieAlgebra line 20
  4. def OAI.Erdos3.FreeNilpotentLieAlgebra.mk line 24
  5. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.mk_surjective line 27
  6. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.mk_eq_zero line 30
  7. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.lowerCentralSeries_eq_bot line 34
  8. def OAI.Erdos3.FreeNilpotentLieAlgebra.of line 40
  9. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.lowerCentralSeries_le_lift_ker line 44
  10. def OAI.Erdos3.FreeNilpotentLieAlgebra.lift line 53
  11. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.lift_mk line 57
  12. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.lift_of line 60
  13. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.hom_ext line 63
  14. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.mk_truncation line 71