OAI/Combinatorics/Progressions/Linear/DualAdjointAction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_zero line 12
2. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_add line 17
3. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_neg line 24
4. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_sub line 29
5. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_one line 33
6. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_mul line 38
7. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_inv_cancel line 44
8. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_cancel_inv line 48
9. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_injective line 52
10. def OAI.Erdos3.NilpotentLieBCHGroup.dualAdjointAddEquiv line 57