OAI/NumberTheory/SiegelZeros/Determinants/NormalDirectionSelection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.normalMap line 17
2. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.exists_kernel_decomposition line 20
3. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.ker_sup_eq_top line 28
4. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.normalMap_surjective line 43
5. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.normalMap_rank line 51
6. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.normalMap_rank_eq_codimension line 56
7. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.kernel_finrank_three line 64
8. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.point_normalMap_injective line 69
9. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.point_normalMap_rank_three line 74
10. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.select_three_directions line 91
11. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.span_normal_basis line 112
12. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.select_normal_directions line 119
13. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.normal_rank_le_three line 132
14. theorem OAI.SiegelZeros.WeightedTorusJets.HyperplaneNormal.select_min_codimension_directions line 141