OAI/NumberTheory/SiegelZeros/Structure/LaurentEvalOne.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.prime_genericPoint_zeroLocus line 15
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.zeroLocus_maximal_of_isMinimalPrime line 19
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isClosed_of_maximal_irreducible_zeroLocus line 37
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.maximal_component_genericPoint line 45
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.shared_minimal_prime_has_generic_component line 56
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.zeroLocus_topologicalKrullDim line 70
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.generic_component_topologicalKrullDim line 81
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.spec_stalk_isLocalRing line 94
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.spec_localization_stalk_regular line 100
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.spec_stalk_component_radical line 107
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.spec_stalk_component_primary line 115
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torusEvalOne_unique line 128
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentEquivLocalization_symm_algebraMap line 160
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentEquivLocalization_polynomial line 165
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentEquivLocalization_inverse_coordinate line 169
  16. def OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentEvalOne line 180
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentEvalOne_polynomial line 183
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentEvalOne_eq_torusEvalOne line 189
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurent_identity_ideal_map line 202
  20. def OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentLocalRingEquivLocalization line 220
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurentLocalRingEquivLocalization_algebraMap line 227
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.spectrum_local_irreducible_dimension_eq_localRing line 244
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_irreducible_closed_subspace_dimension_eq line 281
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.zeroLocus_local_irreducible_dimension_eq_height line 310
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ideal_local_irreducible_dimension_eq_localRing line 337
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurent_ringKrullDim line 371
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.laurent_prime_dimension_codimension line 382
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finiteType_domain_closedPoint_ringKrullDim line 415
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finiteType_prime_component_closedPoint_dimension line 423