OAI/NumberTheory/Ostmann/Characters/TemplateAdaptedCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.Template.coordinateChild line 11
2. theorem OAI.Ostmann.Characters.Template.coordinateChild_map line 17
3. def OAI.Ostmann.Characters.Template.installWords line 24
4. def OAI.Ostmann.Characters.Template.splitWords line 28
5. theorem OAI.Ostmann.Characters.Template.coordinateChild_installWords line 31
6. def OAI.Ostmann.Characters.Template.blockProduct line 62
7. theorem OAI.Ostmann.Characters.Template.blockProduct_map line 66
8. def OAI.Ostmann.Characters.Template.copiedWordEquiv line 70