OAI/NumberTheory/SiegelZeros/EntireFunctions/AffineZeroScheme.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.irrelevant_eq_ker_constantCoeff line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneous_ideal_le_irrelevant line 29
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.irrelevant_isMaximal line 41
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.projectiveSpectrum_lt_irrelevant line 47
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.topologicalKrullDim_le_closure_image line 63
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneProjective_zeroLocus_dimension line 83
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineIntoProj_closure_dimension line 113
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineIntoProj_closure_height_add_dimension line 137
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.projective_component_of_isMinimalPrime line 162
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneProjective_isComponent_of_local_radical line 197
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineIntoProj_closure_isComponent_of_local_radical line 215
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.spec_stalk_cotangent_eq_localization line 244
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_stalk_cotangent_eq_codimension line 260
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_generic_stalk_cotangent_eq_codimension line 282
  15. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroScheme line 304
  16. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeι line 307
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroScheme_isClosedImmersion line 311
  18. def OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientLocalizationEquiv line 315
  19. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeStalkEquiv line 330
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroScheme_range line 338
  21. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemePoint line 345
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemePoint_comap line 350
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemePoint_image line 356
  24. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeStalkEquivAt line 361
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ringEquiv_self_length line 375
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeStalk_length line 381
  27. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeInclusion line 396
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeInclusion_isClosedImmersion line 400
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeInclusion_comp_ι line 404
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemeInclusion_comp line 411
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemePoint_isMinimalPrime line 424
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemePoint_isGenericPoint_component line 433
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineZeroSchemePoint_zeroLocus_image line 445
  34. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusJetZeroScheme line 465
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusJetZeroScheme_isClosedImmersion line 469
  36. def OAI.SiegelZeros.WeightedTorusJets.Geometry.torusJetZeroSchemeStalkEquiv line 475
  37. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusJetZeroSchemeStalk_length line 486