OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedPhaseMatchingGraph.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.Template.OneSidedPhase.anchorCodeEntry line 12
2. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.graph_anchor_entry line 16
3. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.changed_word_code_edge line 24
4. def OAI.Ostmann.Characters.Template.OneSidedPhase.matchingPermutation line 54
5. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.matchingPermutation_bulk line 59
6. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.matchingPermutation_nonword line 64
7. def OAI.Ostmann.Characters.Template.OneSidedPhase.anchorConstituent line 73
8. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.anchorConstituent_role line 79
9. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.matchingPermutation_anchor line 84
10. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.anchorConstituent_fst_ne_bulk line 93