OAI/Combinatorics/Progressions/Nilpotent/DualBCHDifferential.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.NilpotentLieBCHGroup.DualGroup line 12
  2. def OAI.Erdos3.NilpotentLieBCHGroup.dualConstantHom line 15
  3. def OAI.Erdos3.NilpotentLieBCHGroup.dualBaseHom line 18
  4. def OAI.Erdos3.NilpotentLieBCHGroup.dualTangentElement line 21
  5. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualBaseHom_constant line 23
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualBaseHom_tangent line 28
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualTangentElement_injective line 33
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualTangentElement_zero line 37
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualTangentElement_mul line 41
  10. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualTangentElement_neg line 48
  11. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualBaseHom_eq_one_iff line 53
  12. def OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint line 72
  13. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_spec line 76
  14. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_neg_spec line 82
  15. def OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative line 91
  16. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_spec line 94
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_factorization line 99
  18. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_tangent_mul_constant line 105
  19. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_mul line 111
  20. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualBCH_insertion_identity line 127