OAI/NumberTheory/Jacobsthal/Siegel/ConeProjectivePoint.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_chart_prime_height_add_quotient_dim line 14
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finiteType_prime_codimension_nat line 32
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.mul_X_none_pow_mem_coneIdeal_iff line 65
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneMap_of_isHomogeneous line 72
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneous_mem_coneIdeal_iff line 83
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneous_ideal_le_coneIdeal_iff line 97
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneIdeal_eq_homogeneousCore line 120
  8. def OAI.Erdos970.WeightedTorusJets.Geometry.coneProjectivePoint line 136
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneProjectivePoint_mem_basicOpen line 147
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneIdeal_le_iff line 152
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.closure_coneProjectivePoint line 157
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneProjectivePoint_mem_closure_iff line 165
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineProj_homogenizing_mem line 187
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.basicOpenToSpec_coneProjectivePoint line 199
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineIntoProj_polynomial_point line 227
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.closure_affineIntoProj_zeroLocus line 245
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneIdeal_quotient_ringKrullDim line 268
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.projective_zeroLocus_topologicalKrullDim_eq_order line 296
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.projective_zeroLocus_dim_le_of_cone_dim line 312