OAI/NumberTheory/Ostmann/Characters/TemplateDiagonalMatchingCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Characters.TemplateDiagonalMatching.CodePerm line 10
2. theorem OAI.Ostmann.Characters.TemplateDiagonalMatching.codePerm_card_le_product line 13
3. theorem OAI.Ostmann.Characters.TemplateDiagonalMatching.codePerm_card_le line 27
4. def OAI.Ostmann.Characters.TemplateDiagonalMatching.bulkCode line 36
5. def OAI.Ostmann.Characters.TemplateDiagonalMatching.bulkCodeFiberEquiv line 39
6. theorem OAI.Ostmann.Characters.TemplateDiagonalMatching.bulkCode_fiber_card_le line 47
7. theorem OAI.Ostmann.Characters.TemplateDiagonalMatching.bulkCodePerm_card_le line 52