OAI/NumberTheory/SiegelZeros/Characters/Biquadratic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.W10.generators line 19
2. theorem OAI.SiegelZeros.W10.coefficients_eq_zero_of_sign_automorphisms line 21
3. theorem OAI.SiegelZeros.W10.generators_linearIndependent line 47
4. def OAI.SiegelZeros.W10.generatorsBasis line 64
5. theorem OAI.SiegelZeros.W10.generatorsBasis_apply line 74
6. theorem OAI.SiegelZeros.W10.isIntegral_of_square_eq_int line 84
7. theorem OAI.SiegelZeros.W10.generators_isIntegral line 91