OAI/NumberTheory/PiExponent/LocalAlgebra/LocalizationQuotientParameters.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSiegel.W23.quotientParameterPrime line 13
  2. instance OAI.PiExponentSiegel.W23.quotientParameterPrime_isPrime line 16
  3. instance OAI.PiExponentSiegel.W23.quotientParameterPrime_isMaximal line 22
  4. theorem OAI.PiExponentSiegel.W23.mem_quotientParameterPrime_mk line 28
  5. def OAI.PiExponentSiegel.W23.parameterLocalizedIdeal line 32
  6. def OAI.PiExponentSiegel.W23.parameterLocalizationMap line 38
  7. theorem OAI.PiExponentSiegel.W23.parameterLocalizationMap_algebraMap line 48
  8. theorem OAI.PiExponentSiegel.W23.parameterLocalizedIdeal_le_ker line 54
  9. def OAI.PiExponentSiegel.W23.parameterLocalQuotientForward line 62
  10. theorem OAI.PiExponentSiegel.W23.parameterLocalQuotientForward_mk line 69
  11. def OAI.PiExponentSiegel.W23.parameterQuotientToLocalQuotient line 73
  12. theorem OAI.PiExponentSiegel.W23.parameterQuotientToLocalQuotient_mk line 80
  13. theorem OAI.PiExponentSiegel.W23.parameterQuotientToLocalQuotient_units line 85
  14. def OAI.PiExponentSiegel.W23.parameterLocalQuotientReverse line 99
  15. theorem OAI.PiExponentSiegel.W23.parameterLocalQuotientReverse_algebraMap line 106
  16. theorem OAI.PiExponentSiegel.W23.parameterLocalQuotient_reverse_forward line 112
  17. theorem OAI.PiExponentSiegel.W23.parameterLocalQuotient_forward_reverse line 123
  18. def OAI.PiExponentSiegel.W23.localizationQuotientParametersEquiv line 134
  19. theorem OAI.PiExponentSiegel.W23.localizationQuotientParametersEquiv_mk_algebraMap line 144
  20. theorem OAI.PiExponentSiegel.W23.parameterLocalQuotient_isLocalRing line 153
  21. theorem OAI.PiExponentSiegel.W23.localizationQuotientParametersEquiv_maximalIdeal line 157
  22. def OAI.PiExponentSiegel.W23.localizationQuotientParametersResidueEquiv line 165
  23. theorem OAI.PiExponentSiegel.W23.localizationQuotientParametersResidueEquiv_residue line 172
  24. theorem OAI.PiExponentSiegel.W23.parameterLocalizedIdeal_span_singleton line 184
  25. theorem OAI.PiExponentSiegel.W23.atPrimeImage_comap line 195
  26. def OAI.PiExponentSiegel.W23.atPrimeEquivOfRingEquiv line 201
  27. theorem OAI.PiExponentSiegel.W23.atPrimeEquivOfRingEquiv_algebraMap line 206
  28. def OAI.PiExponentSiegel.W23.localizationQuotientParametersEquivTrans line 214
  29. theorem OAI.PiExponentSiegel.W23.localizationQuotientParametersEquivTrans_mk_algebraMap line 220