OAI/NumberTheory/Ostmann/Characters/TemplateAmplitudeRecurrenceNodeSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Characters.Template.CurrentAtomSupport.source_pivot_pos line 12
2. theorem OAI.Ostmann.Characters.Template.CurrentAtomSupport.source_pivot_coprime line 19
3. theorem OAI.Ostmann.Characters.Template.CurrentAtomSupport.copiedProduct_coprime line 26
4. theorem OAI.Ostmann.Characters.Template.CurrentAtomSupport.copiedProduct_unit line 33
5. theorem OAI.Ostmann.Characters.Template.reconstructedPivot_pairedState_of_reversal line 39
6. theorem OAI.Ostmann.Characters.Template.nodeSupports_pairedState_of_reversal line 46