OAI/Combinatorics/Progressions/Estimates/LieFiniteProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Erdos3.lieRingPi line 13
  2. theorem OAI.Erdos3.lie_pi_apply line 20
  3. instance OAI.Erdos3.lieAlgebraPi line 24
  4. def OAI.Erdos3.liePiEval line 27
  5. theorem OAI.Erdos3.liePiEval_apply line 31
  6. def OAI.Erdos3.liePiMap line 35
  7. theorem OAI.Erdos3.liePiMap_apply line 39
  8. theorem OAI.Erdos3.liePiEval_comp_liePiMap line 42
  9. def OAI.Erdos3.NilpotentLieFiltration.pi line 49
  10. theorem OAI.Erdos3.NilpotentLieFiltration.mem_pi_layer line 56
  11. theorem OAI.Erdos3.lie_pi_structure_height line 68
  12. theorem OAI.Erdos3.liePiMap_height line 90