OAI/NumberTheory/SiegelZeros/Structure/GaussLegendre.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.Awei.W39.intCast_ne_zero_of_not_dvd_natAbs line 11
2. theorem OAI.SiegelZeros.Awei.W39.frobenius_eigenvalue_eq_legendre line 18
3. theorem OAI.SiegelZeros.Awei.W39.integerCharacter_legendre_of_gaussSum_sq line 42