OAI/GroupTheory/Kervaire/WordNormalization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KervaireRibbon.syllableEval line 11
2. def OAI.KervaireRibbon.UnitSyllables line 14
3. def OAI.KervaireRibbon.Normalized line 16
4. lemma OAI.KervaireRibbon.Normalized.one line 19
5. lemma OAI.KervaireRibbon.Normalized.prependCoefficient line 22
6. lemma OAI.KervaireRibbon.Normalized.prependLetter line 27
7. lemma OAI.KervaireRibbon.Normalized.prependPower line 37
8. lemma OAI.KervaireRibbon.normalized_every line 50
9. lemma OAI.KervaireRibbon.unit_syllables_every line 58

   Source documentation

   Inserting the actually trivial pair t·t⁻¹ absorbs the leading coefficient. This is equality in the unchanged free product, not a new group relation.

   lemma unit_syllables_every (w : FreeProd A) :
       ∃ l : List (ℤ × A), 2 ≤ l.length ∧ UnitSyllables l ∧ syllableEval l = w := by
   …

   Mentions: OAI.KervaireRibbon.FreeProd, OAI.KervaireRibbon.UnitSyllables, OAI.KervaireRibbon.syllableEval

10. lemma OAI.KervaireRibbon.syllableEval_exponent line 72
11. lemma OAI.KervaireRibbon.circle_formPerm line 85
12. lemma OAI.KervaireRibbon.formPerm_sameCycle_all line 101