OAI/NumberTheory/SiegelZeros/Characters/ExceptionalConductor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W56.character_nat_eq_of_prime_eq line 15
2. theorem OAI.SiegelZeros.W56.changeLevel_eq_of_prime_eq line 33
3. theorem OAI.SiegelZeros.W56.primitive_levels_eq_of_changeLevel_eq line 51
4. def OAI.SiegelZeros.W56.chiEightComplex line 79
5. theorem OAI.SiegelZeros.W56.chiEightComplex_apply line 82
6. theorem OAI.SiegelZeros.W56.chiEightComplex_not_factorsThrough line 85
7. theorem OAI.SiegelZeros.W56.chiEightComplex_isPrimitive line 96
8. theorem OAI.SiegelZeros.W56.conductor_eight_of_prime_values line 108