OAI/NumberTheory/SiegelZeros/LocalAlgebra/CanonicalQuotient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedQuotient line 18
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedQuotient_meromorphic line 21
3. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.meromorphicOrderAt_normalizedQuotient_eq_zero line 28
4. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedQuotient_entire_ne_zero line 43
5. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedQuotient_eq_div line 59
6. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedQuotient_mul line 70
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.exists_entire_logarithm_normalizedQuotient line 82