OAI/Analysis/Kaplansky/Regular/FreeWord.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.Regular.toWord_translate line 12
2. lemma OAI.KaplanskyConsequences.Regular.toWord_mul_of_boundary line 23
3. lemma OAI.KaplanskyConsequences.Regular.toWord_inv_of line 31
4. def OAI.KaplanskyConsequences.Regular.Starts line 34
5. lemma OAI.KaplanskyConsequences.Regular.starts_iff_head line 36
6. lemma OAI.KaplanskyConsequences.Regular.not_starts_head line 38
7. lemma OAI.KaplanskyConsequences.Regular.starts_translate line 45
8. lemma OAI.KaplanskyConsequences.Regular.prefix_multiply_of_not_starts line 58
9. lemma OAI.KaplanskyConsequences.Regular.word_sandwich line 62
10. lemma OAI.KaplanskyConsequences.Regular.sandwich_multiply_starts line 95