OAI/NumberTheory/SiegelZeros/LocalAlgebra/ConeQuotientAugmentation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.SiegelZerosAwei.W30.coneDifferential line 19
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneDifferential_apply line 24
3. def OAI.SiegelZeros.SiegelZerosAwei.W30.coneBottom line 28
4. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneBottom_apply line 31
5. lemma OAI.SiegelZeros.SiegelZerosAwei.W30.comp_zero_of_range_eq_ker line 34
6. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneDifferential_comp line 43
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneDifferential_exact line 56
8. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneBottom_exact line 92
9. def OAI.SiegelZeros.SiegelZerosAwei.W30.coneQuotientAugmentation line 143
10. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneQuotientAugmentation_exact line 146
11. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneQuotientAugmentation_surjective line 174