OAI/NumberTheory/PiExponent/LocalAlgebra/AffineClosedPointLocalization.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSiegel.W23.affineCoefficientAlgHom line 16
  2. abbrev OAI.PiExponentSiegel.W23.affineCoefficientMap line 22
  3. def OAI.PiExponentSiegel.W23.affineCoefficientAlgebra line 26
  4. instance OAI.PiExponentSiegel.W23.affineCoefficient_isLocalization line 32
  5. def OAI.PiExponentSiegel.W23.affineMappedIdeal line 38
  6. theorem OAI.PiExponentSiegel.W23.affineCoefficientMap_comap_closedPoint line 45
  7. theorem OAI.PiExponentSiegel.W23.affineDenominators_disjoint line 56
  8. theorem OAI.PiExponentSiegel.W23.affineMappedIdeal_isPrime line 68
  9. theorem OAI.PiExponentSiegel.W23.affineMappedIdeal_le_closedPoint line 74
  10. theorem OAI.PiExponentSiegel.W23.affineMappedIdeal_comap line 82
  11. theorem OAI.PiExponentSiegel.W23.originalLocalCoefficientLocalEquiv_algebraMap line 89
  12. theorem OAI.PiExponentSiegel.W23.closedPointLocalEquiv_algebraMap line 97
  13. theorem OAI.PiExponentSiegel.W23.closedPointLocalEquiv_map_ideal line 117
  14. def OAI.PiExponentSiegel.W23.affineLocalQuotientEquiv line 129
  15. def OAI.PiExponentSiegel.W23.affineClosedQuotientLocalEquiv line 137
  16. def OAI.PiExponentSiegel.W23.affineQuotientMap line 150
  17. def OAI.PiExponentSiegel.W23.affineQuotientAlgebra line 155
  18. theorem OAI.PiExponentSiegel.W23.affineQuotientMap_mk line 167
  19. instance OAI.PiExponentSiegel.W23.affineQuotient_scalarTower line 172
  20. theorem OAI.PiExponentSiegel.W23.affineQuotientMap_injective line 187
  21. theorem OAI.PiExponentSiegel.W23.affineQuotient_faithfulSMul line 193
  22. theorem OAI.PiExponentSiegel.W23.affineQuotient_isDomain line 202
  23. theorem OAI.PiExponentSiegel.W23.affineQuotient_finiteType line 208
  24. theorem OAI.PiExponentSiegel.W23.affineQuotient_isLocalization line 217
  25. theorem OAI.PiExponentSiegel.W23.affineClosedQuotientLocalEquiv_mk_algebraMap line 248