OAI/NumberTheory/SiegelZeros/Structure/KoszulDualInitial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SiegelZeros.SiegelZerosAwei.W30.range_comp_eq_of_surjective line 17
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalar_sub_range line 27
3. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_top_dual_image line 51
4. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.regular_on_dual line 88
5. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coordinate_quotient_exact line 96
6. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coordinate_quotient_surjective line 112
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_dual_zero_injective_of_regular line 119
8. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_dual_zero_injective line 134
9. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_first_top_dual_image line 150