OAI/Analysis/Commutator/ConjugatedWordAlgebra.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FinitePatching.ConjugatedWords.signPower line 21
2. def OAI.Kadison.FinitePatching.ConjugatedWords.leftUnitary line 23
3. def OAI.Kadison.FinitePatching.ConjugatedWords.transition line 25
4. def OAI.Kadison.FinitePatching.ConjugatedWords.front line 27
5. def OAI.Kadison.FinitePatching.ConjugatedWords.encode line 31
6. lemma OAI.Kadison.FinitePatching.ConjugatedWords.transition_power line 36
7. lemma OAI.Kadison.FinitePatching.ConjugatedWords.encode_length line 44
8. lemma OAI.Kadison.FinitePatching.ConjugatedWords.encode_ne_nil line 50
9. lemma OAI.Kadison.FinitePatching.ConjugatedWords.encode_valid line 57
10. lemma OAI.Kadison.FinitePatching.ConjugatedWords.word_encode line 78