OAI/NumberTheory/Ostmann/Supply/GroupedCharactersPrimitive.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Supply.GroupedCharacters.boundedCharacter line 17
2. theorem OAI.Ostmann.Supply.GroupedCharacters.boundedCharacter_injective line 28
3. theorem OAI.Ostmann.Supply.GroupedCharacters.boundedCharacter_conductor line 35
4. theorem OAI.Ostmann.Supply.GroupedCharacters.boundedCharacter_apply line 40
5. def OAI.Ostmann.Supply.GroupedCharacters.primitiveCoefficient line 46
6. theorem OAI.Ostmann.Supply.GroupedCharacters.grouped_sum_univ line 50
7. theorem OAI.Ostmann.Supply.GroupedCharacters.primitive_weight_expansion line 61
8. def OAI.Ostmann.Supply.GroupedCharacters.principalTuple line 73
9. def OAI.Ostmann.Supply.GroupedCharacters.principalCharacter line 76
10. theorem OAI.Ostmann.Supply.GroupedCharacters.boundedCharacter_principal line 79
11. theorem OAI.Ostmann.Supply.GroupedCharacters.primitiveCoefficient_principal line 85