OAI/NumberTheory/SiegelZeros/Intersection/ConeProjectivePoint.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_chart_prime_height_add_quotient_dim line 16
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finiteType_prime_codimension_nat line 38
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.mul_X_none_pow_mem_coneIdeal_iff line 104
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneMap_of_isHomogeneous line 111
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneous_mem_coneIdeal_iff line 122
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneous_ideal_le_coneIdeal_iff line 136
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneIdeal_eq_homogeneousCore line 159
  8. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneProjectivePoint line 175
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneProjectivePoint_mem_basicOpen line 186
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneIdeal_le_iff line 191
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.closure_coneProjectivePoint line 196
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneProjectivePoint_mem_closure_iff line 204
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineProj_homogenizing_mem line 240
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.basicOpenToSpec_coneProjectivePoint line 252
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineIntoProj_polynomial_point line 280
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.closure_affineIntoProj_zeroLocus line 298
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneIdeal_quotient_ringKrullDim line 322
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.projective_zeroLocus_topologicalKrullDim_eq_order line 354
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.projective_zeroLocus_dim_le_of_cone_dim line 370