OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedPhaseAction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.Template.OneSidedPhase.bulkEmbedding line 12
  2. def OAI.Ostmann.Characters.Template.OneSidedPhase.constituentPermutation line 22
  3. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.constituentPermutation_bulk line 26
  4. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.constituentPermutation_nonword line 32
  5. def OAI.Ostmann.Characters.Template.OneSidedPhase.smallAnchorConstituent line 41
  6. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.smallAnchorConstituent_role line 47
  7. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.constituentPermutation_anchor line 52
  8. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.constituentGraph_of_fst_ne line 61
  9. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.anchor_fst_ne_bulk line 67
  10. theorem OAI.Ostmann.Characters.Template.OneSidedPhase.distinct_reassignments_constituent_edge line 78