OAI/NumberTheory/Ostmann/Characters/TemplateOutgoingPivot.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Characters.Template.InputPrimeIndex line 11
2. def OAI.Ostmann.Characters.Template.inputCopiedProduct line 13
3. def OAI.Ostmann.Characters.Template.inputOutsideProduct line 14
4. def OAI.Ostmann.Characters.Template.pivotOutsideComplement line 15
5. theorem OAI.Ostmann.Characters.Template.otherProduct_pivot line 18
6. def OAI.Ostmann.Characters.Template.outgoingPivotFactor line 30
7. theorem OAI.Ostmann.Characters.Template.outgoing_pivot_factorization line 34