OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedPhaseTerminalIndexedSource.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Characters.Template.OneSidedPhase.sourceTerminalCharactersline 21 - def
OAI.Ostmann.Characters.Template.OneSidedPhase.sourceTerminalGraphline 23 - def
OAI.Ostmann.Characters.Template.OneSidedPhase.sourceTerminalPairedUnaryline 27 - theorem
OAI.Ostmann.Characters.Template.OneSidedPhase.sourceTerminalPhasePair_eq_graphline 33