OAI/NumberTheory/SiegelZeros/Intersection/PrimeHypersurfaceEquidimension.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W24.proper_prime_cut_dimension_succ_le line 26
2. theorem OAI.SiegelZeros.WeightedTorusJets.W24.proper_prime_cut_dimension_le line 38
3. theorem OAI.SiegelZeros.WeightedTorusJets.W24.proper_prime_cut_relative_height_eq_one line 53
4. theorem OAI.SiegelZeros.WeightedTorusJets.W24.proper_prime_cut_relative_local_dimension line 77
5. theorem OAI.SiegelZeros.WeightedTorusJets.W24.minimal_proper_prime_cut_dimension_le line 96
6. theorem OAI.SiegelZeros.WeightedTorusJets.W29.under_height_le_of_goingDown line 119
7. theorem OAI.SiegelZeros.WeightedTorusJets.W29.affineDomain_maximal_height line 140
8. theorem OAI.SiegelZeros.WeightedTorusJets.W29.closedPoint_local_dimension line 164
9. theorem OAI.SiegelZeros.WeightedTorusJets.W24.affine_prime_dimension_of_closedPoint_presentation line 180
10. theorem OAI.SiegelZeros.WeightedTorusJets.W24.ringEquiv_localizedIdeal_map line 222
11. def OAI.SiegelZeros.WeightedTorusJets.W24.ringEquiv_localQuotient line 233
12. theorem OAI.SiegelZeros.WeightedTorusJets.W24.split_polynomial_prime_pair_local_dimension line 246
13. theorem OAI.SiegelZeros.WeightedTorusJets.W24.fin_polynomial_prime_pair_local_dimension line 293
14. theorem OAI.SiegelZeros.WeightedTorusJets.W24.polynomial_prime_pair_local_dimension line 321
15. theorem OAI.SiegelZeros.WeightedTorusJets.W24.polynomial_prime_pair_dimension line 340
16. theorem OAI.SiegelZeros.WeightedTorusJets.W24.minimal_prime_hypersurface_dimension line 364