OAI/Analysis/FreeWords/HaarTwistEndpoints.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KKFreeWords.powerBlocks_chain_last_free line 115
2. theorem OAI.KKFreeWords.trace_twisted_signedWord line 129
3. def OAI.KKFreeWords.signedMulLast line 142
4. theorem OAI.KKFreeWords.signedMulLast_value line 148
5. theorem OAI.KKFreeWords.signedMulLast_ne_nil line 160
6. theorem OAI.KKFreeWords.signedMulLast_mem line 167
7. theorem OAI.KKFreeWords.signedMulLast_chain line 187