OAI/Analysis/Commutator/FreeSymmetry10.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FreeBlocks.pullbackState line 36
2. lemma OAI.Kadison.FreeBlocks.pullbackState_apply line 50
3. def OAI.Kadison.FreeBlocks.factorPreMap line 55
4. lemma OAI.Kadison.FreeBlocks.factorPreMap_surjective line 68
5. def OAI.Kadison.FreeBlocks.factorPreIso line 78
6. def OAI.Kadison.FreeBlocks.factorGNSIso line 82
7. lemma OAI.Kadison.FreeBlocks.factorGNSIso_coe line 86