OAI/Analysis/Commutator/FreeInnerFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FreeWordAction.innerFamily line 28
2. lemma OAI.Kadison.FreeWordAction.innerFamily_self line 34
3. lemma OAI.Kadison.FreeWordAction.innerFamily_other line 39
4. lemma OAI.Kadison.FreeWordAction.innerFamily_mem line 44
5. lemma OAI.Kadison.FreeWordAction.innerFamily_trace line 55
6. lemma OAI.Kadison.FreeWordAction.innerFamily_one line 64
7. lemma OAI.Kadison.FreeWordAction.innerFamily_mul line 70
8. lemma OAI.Kadison.FreeWordAction.innerFamily_continuous line 82