OAI/NumberTheory/SiegelZeros/Structure/SignedDiscriminant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.Awei.W39.signedOddDiscriminant line 11
2. theorem OAI.SiegelZeros.Awei.W39.signedOddDiscriminant_one_mod_four line 13
3. theorem OAI.SiegelZeros.Awei.W39.signedOddDiscriminant_three_mod_four line 17
4. theorem OAI.SiegelZeros.Awei.W39.legendre_signedOddDiscriminant line 21
5. theorem OAI.SiegelZeros.Awei.W39.legendre_remove_square_factor line 29
6. theorem OAI.SiegelZeros.Awei.W39.legendre_four_mul line 38
7. theorem OAI.SiegelZeros.Awei.W39.legendre_neg_four_signedOddDiscriminant line 49
8. theorem OAI.SiegelZeros.Awei.W39.legendre_eight_signedOddDiscriminant line 58
9. theorem OAI.SiegelZeros.Awei.W39.legendre_neg_eight_signedOddDiscriminant line 67