OAI/NumberTheory/Jacobsthal/Siegel/AffineZeroScheme.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.irrelevant_eq_ker_constantCoeff line 18
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneous_ideal_le_irrelevant line 28
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.irrelevant_isMaximal line 40
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.projectiveSpectrum_lt_irrelevant line 46
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.topologicalKrullDim_le_closure_image line 60
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneProjective_zeroLocus_dimension line 76
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineIntoProj_closure_dimension line 106
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineIntoProj_closure_height_add_dimension line 128
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.projective_component_of_isMinimalPrime line 151
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneProjective_isComponent_of_local_radical line 184
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineIntoProj_closure_isComponent_of_local_radical line 202
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.spec_stalk_cotangent_eq_localization line 229
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_stalk_cotangent_eq_codimension line 245
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_generic_stalk_cotangent_eq_codimension line 267
  15. def OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroScheme line 289
  16. def OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeι line 292
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroScheme_isClosedImmersion line 296
  18. def OAI.Erdos970.WeightedTorusJets.Geometry.quotientLocalizationEquiv line 300
  19. def OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeStalkEquiv line 315
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroScheme_range line 323
  21. def OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemePoint line 330
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemePoint_comap line 335
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemePoint_image line 341
  24. def OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeStalkEquivAt line 346
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ringEquiv_self_length line 360
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeStalk_length line 366
  27. def OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeInclusion line 379
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeInclusion_isClosedImmersion line 383
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeInclusion_comp_ι line 387
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemeInclusion_comp line 394
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemePoint_isMinimalPrime line 405
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemePoint_isGenericPoint_component line 414
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineZeroSchemePoint_zeroLocus_image line 426
  34. def OAI.Erdos970.WeightedTorusJets.Geometry.torusJetZeroScheme line 443
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusJetZeroScheme_isClosedImmersion line 447
  36. def OAI.Erdos970.WeightedTorusJets.Geometry.torusJetZeroSchemeStalkEquiv line 453
  37. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusJetZeroSchemeStalk_length line 464