OAI/NumberTheory/Jacobsthal/Siegel/LaurentEvalOne.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.prime_genericPoint_zeroLocus line 14
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.zeroLocus_maximal_of_isMinimalPrime line 18
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isClosed_of_maximal_irreducible_zeroLocus line 36
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.maximal_component_genericPoint line 44
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.shared_minimal_prime_has_generic_component line 55
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.zeroLocus_topologicalKrullDim line 67
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.generic_component_topologicalKrullDim line 78
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.spec_stalk_isLocalRing line 89
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.spec_localization_stalk_regular line 95
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.spec_stalk_component_radical line 102
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.spec_stalk_component_primary line 110
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torusEvalOne_unique line 121
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurentEquivLocalization_symm_algebraMap line 152
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurentEquivLocalization_polynomial line 157
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurentEquivLocalization_inverse_coordinate line 161
  16. def OAI.Erdos970.WeightedTorusJets.Geometry.laurentEvalOne line 172
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurentEvalOne_polynomial line 175
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurentEvalOne_eq_torusEvalOne line 181
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurent_identity_ideal_map line 194
  20. def OAI.Erdos970.WeightedTorusJets.Geometry.laurentLocalRingEquivLocalization line 210
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurentLocalRingEquivLocalization_algebraMap line 217
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.spectrum_local_irreducible_dimension_eq_localRing line 232
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_irreducible_closed_subspace_dimension_eq line 265
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.zeroLocus_local_irreducible_dimension_eq_height line 294
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ideal_local_irreducible_dimension_eq_localRing line 321
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurent_ringKrullDim line 349
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.laurent_prime_dimension_codimension line 360
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finiteType_domain_closedPoint_ringKrullDim line 387
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finiteType_prime_component_closedPoint_dimension line 395