OAI/Combinatorics/Progressions/Linear/DualIdealSteps.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.dualConstant_infinitesimal_lie line 14
  2. theorem OAI.Erdos3.dualInfinitesimal_constant_lie line 20
  3. theorem OAI.Erdos3.dualTangentLinear_lie line 26
  4. def OAI.Erdos3.dualIdealSubalgebra line 47
  5. theorem OAI.Erdos3.mem_dualIdealSubalgebra line 55
  6. def OAI.Erdos3.dualIdealRealization line 58
  7. theorem OAI.Erdos3.dualIdealRealization_apply line 83
  8. def OAI.Erdos3.dualQuotientEvaluate line 88
  9. theorem OAI.Erdos3.dualQuotientEvaluate_apply line 91
  10. theorem OAI.Erdos3.dualQuotientEvaluate_constant line 94
  11. theorem OAI.Erdos3.dualQuotientEvaluate_infinitesimal line 98
  12. theorem OAI.Erdos3.dualQuotientEvaluate_lieBCH line 102
  13. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_conjugation_mod line 122
  14. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_eq_conjugation_of_abelian_ideal line 150
  15. def OAI.Erdos3.dualCoordinates line 168
  16. theorem OAI.Erdos3.dualCoordinates_apply line 174
  17. theorem OAI.Erdos3.dualCoordinates_symm_apply line 177
  18. def OAI.Erdos3.dualFirstOrderIdeal line 187
  19. def OAI.Erdos3.DualFirstOrderCongruent line 197
  20. theorem OAI.Erdos3.dualFirstOrderCongruent_lieBCH line 200
  21. theorem OAI.Erdos3.dualFirstOrderCongruent_constant line 230
  22. theorem OAI.Erdos3.dualFirstOrderCongruent_infinitesimal line 237
  23. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_sub_mem line 248
  24. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_sub_mem line 269
  25. theorem OAI.Erdos3.dual_ext line 308
  26. def OAI.Erdos3.dualLinearLift line 315
  27. theorem OAI.Erdos3.dualLinearLift_apply line 320
  28. theorem OAI.Erdos3.dualLinearLift_base line 324
  29. theorem OAI.Erdos3.dualLinearLift_tangent line 328
  30. theorem OAI.Erdos3.dualLinearLift_constant line 332
  31. theorem OAI.Erdos3.dualLinearLift_infinitesimal line 337
  32. theorem OAI.Erdos3.dualIdealMorphism_left line 346
  33. def OAI.Erdos3.dualIdealMorphism line 352
  34. theorem OAI.Erdos3.dualLinearLift_lieBCH line 368
  35. instance OAI.Erdos3.dualRealModule line 385
  36. def OAI.Erdos3.dualRealCoordinates line 388
  37. theorem OAI.Erdos3.dualRealCoordinates_apply line 391
  38. theorem OAI.Erdos3.dualRealCoordinates_symm_apply line 394
  39. theorem OAI.Erdos3.dualBaseLinear_smul_real line 397
  40. theorem OAI.Erdos3.dualTangentLinear_smul_real line 401
  41. instance OAI.Erdos3.dualRealScalarTower line 405
  42. instance OAI.Erdos3.dualRealLieAlgebra line 410
  43. theorem OAI.Erdos3.NilpotentLieBCHGroup.map_coord line 429
  44. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLinearLift_logDerivative line 433
  45. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLinearLift_adjoint line 451
  46. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLinearLift_logDerivative_eq line 469
  47. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLinearLift_adjoint_eq line 478
  48. def OAI.Erdos3.dualInvariantSubalgebra line 494
  49. theorem OAI.Erdos3.mem_dualInvariantSubalgebra line 509
  50. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_mem_of_invariant line 518
  51. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_mem_of_invariant line 532
  52. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_mem_ideal line 544
  53. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_mem_ideal line 548
  54. theorem OAI.Erdos3.dualLinearLift_lieBCH_of_steps line 565
  55. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLinearLift_adjoint_of_steps line 582
  56. theorem OAI.Erdos3.NilpotentLieBCHGroup.mapOfSteps_dualAdjoint line 600