OAI/NumberTheory/SiegelZeros/LocalAlgebra/ResidueField.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.SiegelZerosAwei.W38.exists_maximal_above_prime line 17
2. def OAI.SiegelZeros.SiegelZerosAwei.W38.primeIdealAbove line 21
3. instance OAI.SiegelZeros.SiegelZerosAwei.W38.primeIdealAbove_isMaximal line 24
4. instance OAI.SiegelZeros.SiegelZerosAwei.W38.primeIdealAbove_liesOver line 27
5. abbrev OAI.SiegelZeros.SiegelZerosAwei.W38.PrimeResidueField line 31
6. instance OAI.SiegelZeros.SiegelZerosAwei.W38.primeResidueField_field line 33
7. instance OAI.SiegelZeros.SiegelZerosAwei.W38.primeResidueField_charP line 36
8. def OAI.SiegelZeros.SiegelZerosAwei.W38.primeReduction line 45
9. theorem OAI.SiegelZeros.SiegelZerosAwei.W38.residue_natCast_ne_zero line 48
10. theorem OAI.SiegelZeros.SiegelZerosAwei.W38.primeReduction_natCast_ne_zero line 52