OAI/NumberTheory/SiegelZeros/Determinants/NormalizedCompletion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedCompletion line 17
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.conductorFactor_ne_zero line 20
3. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.differentiable_conductorFactor line 23
4. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.differentiable_normalizedCompletion line 28
5. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedCompletion_zero_iff line 32
6. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.LFunction_zero_iff_normalizedCompletion_zero line 36
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedCompletion_ne_zero_of_one_le_re line 42
8. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedCompletion_one_sub line 49
9. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.logDeriv_conductorFactor line 69
10. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.logDeriv_normalizedCompletion line 77