OAI/Analysis/Commutator/FreeActionBlock.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FreeBlocks.mapBlockD line 26
2. lemma OAI.Kadison.FreeBlocks.paramD_mapBlockD line 31
3. lemma OAI.Kadison.FreeBlocks.paramJ_mapBlockD line 40
4. lemma OAI.Kadison.FreeBlocks.action_left_apply line 57
5. lemma OAI.Kadison.FreeBlocks.action_algebra_of_mem line 63
6. lemma OAI.Kadison.FreeBlocks.action_vector_mul line 69
7. lemma OAI.Kadison.FreeBlocks.action_blockRead_pure line 77