OAI/NumberTheory/SiegelZeros/LocalAlgebra/AffineClosedPointLocalization.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.coefficientClosedPoint line 21
  2. instance OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.coefficientClosedPoint_isMaximal line 26
  3. abbrev OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.CoefficientClosedLocal line 34
  4. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.closedLocal_isLocalizationAtOriginal line 36
  5. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.originalLocalCoefficientLocalEquiv line 55
  6. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.closedPolynomialIdeal line 61
  7. instance OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.closedPolynomialIdeal_isMaximal line 65
  8. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.polynomialPrimeClosedPointEquiv line 71
  9. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.polynomialPrimeClosedPointResidueEquiv line 79
  10. def OAI.SiegelZeros.W23.affineCoefficientAlgHom line 100
  11. abbrev OAI.SiegelZeros.W23.affineCoefficientMap line 106
  12. def OAI.SiegelZeros.W23.affineCoefficientAlgebra line 110
  13. instance OAI.SiegelZeros.W23.affineCoefficient_isLocalization line 116
  14. def OAI.SiegelZeros.W23.affineMappedIdeal line 122
  15. theorem OAI.SiegelZeros.W23.affineCoefficientMap_comap_closedPoint line 129
  16. theorem OAI.SiegelZeros.W23.affineDenominators_disjoint line 140
  17. theorem OAI.SiegelZeros.W23.affineMappedIdeal_isPrime line 152
  18. theorem OAI.SiegelZeros.W23.affineMappedIdeal_le_closedPoint line 158
  19. theorem OAI.SiegelZeros.W23.affineMappedIdeal_comap line 166
  20. theorem OAI.SiegelZeros.W23.originalLocalCoefficientLocalEquiv_algebraMap line 173
  21. theorem OAI.SiegelZeros.W23.closedPointLocalEquiv_algebraMap line 181
  22. theorem OAI.SiegelZeros.W23.closedPointLocalEquiv_map_ideal line 207
  23. def OAI.SiegelZeros.W23.affineLocalQuotientEquiv line 219
  24. def OAI.SiegelZeros.W23.affineClosedQuotientLocalEquiv line 227
  25. def OAI.SiegelZeros.W23.affineQuotientMap line 240
  26. def OAI.SiegelZeros.W23.affineQuotientAlgebra line 245
  27. theorem OAI.SiegelZeros.W23.affineQuotientMap_mk line 257
  28. instance OAI.SiegelZeros.W23.affineQuotient_scalarTower line 262
  29. theorem OAI.SiegelZeros.W23.affineQuotientMap_injective line 277
  30. theorem OAI.SiegelZeros.W23.affineQuotient_faithfulSMul line 283
  31. theorem OAI.SiegelZeros.W23.affineQuotient_isDomain line 292
  32. theorem OAI.SiegelZeros.W23.affineQuotient_finiteType line 298
  33. theorem OAI.SiegelZeros.W23.affineQuotient_isLocalization line 307
  34. theorem OAI.SiegelZeros.W23.affineClosedQuotientLocalEquiv_mk_algebraMap line 338