OAI/Combinatorics/Progressions/Nilpotent/FreeWeightedNilpotentLieAlgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FreeWeightedNilpotentLieAlgebra line 9
  2. instance OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.instLieRing line 16
  3. instance OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.instLieAlgebra line 20
  4. def OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.mk line 24
  5. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.mk_surjective line 27
  6. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.mk_eq_zero line 29
  7. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.lowerCentralSeries_eq_bot line 33
  8. def OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.of line 38
  9. def OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.filtration line 41
  10. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.of_mem_layer line 56
  11. instance OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.finite line 61
  12. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.finrank_le line 64