OAI/Combinatorics/Progressions/Nilpotent/FilteredAdjointFirstBracket.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentAlgebraFiltration.mul_eq_zero_of_degrees line 13
  2. theorem OAI.Erdos3.NilpotentAlgebraFiltration.exp_eq_quadratic line 18
  3. theorem OAI.Erdos3.NilpotentAlgebraFiltration.nilpotentBCH_eq_quadratic line 23
  4. theorem OAI.Erdos3.lieBCH_eq_quadratic_of_step_two line 62
  5. def OAI.Erdos3.centralPairSpan line 88
  6. theorem OAI.Erdos3.centralPairSpan_lie_mem line 91
  7. theorem OAI.Erdos3.centralPairSpan_lie_eq_zero line 118
  8. def OAI.Erdos3.centralPairSubalgebra line 137
  9. theorem OAI.Erdos3.centralPairSubalgebra_step_two line 143
  10. theorem OAI.Erdos3.lieBCH_eq_quadratic_of_central_commutator line 161
  11. theorem OAI.Erdos3.lieBCH_conjugation_of_central_commutator line 172
  12. theorem OAI.Erdos3.lieBCH_conjugation_sub_mem line 187
  13. def OAI.Erdos3.dualBaseSubalgebra line 209
  14. def OAI.Erdos3.dualInvariantTangentIdeal line 213
  15. theorem OAI.Erdos3.mem_dualInvariantTangentIdeal line 224
  16. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_eq_add_lie line 234
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_sub_first_bracket_mem line 246
  18. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_current_bracket_relation line 287
  19. theorem OAI.Erdos3.NilpotentLieFiltration.dualAdjoint_sub_first_bracket_mem_layer line 313
  20. def OAI.Erdos3.polynomialDualEval line 335
  21. theorem OAI.Erdos3.polynomialDualEval_constant line 354
  22. theorem OAI.Erdos3.polynomialDualEval_linear line 361
  23. theorem OAI.Erdos3.NilpotentLieBCHGroup.conjugation_polynomial line 372
  24. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_eq_conjugationCoord line 383
  25. theorem OAI.Erdos3.NilpotentLieBCHGroup.conjugationCoord_eq_add_lie line 391
  26. theorem OAI.Erdos3.NilpotentLieFiltration.invariant_sup_layer line 415
  27. theorem OAI.Erdos3.NilpotentLieFiltration.lie_mem_invariant_sup_next_layer line 423
  28. theorem OAI.Erdos3.NilpotentLieFiltration.adjoint_current_layer_relation line 432
  29. theorem OAI.Erdos3.NilpotentLieFiltration.adjoint_current_layer_quotient line 449