OAI/NumberTheory/SiegelZeros/Determinants/NormalSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.ActualNormalSelection.shrink_independent line 17
2. theorem OAI.SiegelZeros.WeightedTorusJets.ActualNormalSelection.ideal_derivative_evaluation_surjective line 26
3. abbrev OAI.SiegelZeros.WeightedTorusJets.ActualNormalSelection.GenericResidue line 44
4. abbrev OAI.SiegelZeros.WeightedTorusJets.ActualNormalSelection.GenericMaximal line 45
5. def OAI.SiegelZeros.WeightedTorusJets.ActualNormalSelection.genericCoordinates line 63
6. theorem OAI.SiegelZeros.WeightedTorusJets.ActualNormalSelection.generic_height_selected_normals line 74
7. theorem OAI.SiegelZeros.WeightedTorusJets.ActualNormalSelection.generic_original_direction_selection line 113
8. theorem OAI.SiegelZeros.WeightedTorusJets.ActualNormalSelection.identity_three_selected_normals line 159