OAI/NumberTheory/SiegelZeros/LocalAlgebra/DVRLocalCoordinates.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.W58.parameterIdeal line 24
  2. instance OAI.SiegelZeros.W58.parameterIdeal_isMaximal line 26
  3. abbrev OAI.SiegelZeros.W58.ParameterLocalRing line 30
  4. lemma OAI.SiegelZeros.W58.parameterIdeal_eq_span_X line 32
  5. lemma OAI.SiegelZeros.W58.parameterIdeal_mem_iff line 35
  6. lemma OAI.SiegelZeros.W58.nonunit_transcendental line 40
  7. lemma OAI.SiegelZeros.W58.uniformizer_aeval_injective line 45
  8. lemma OAI.SiegelZeros.W58.uniformizer_residue_zero line 51
  9. lemma OAI.SiegelZeros.W58.residue_aeval_uniformizer line 57
  10. lemma OAI.SiegelZeros.W58.uniformizer_aeval_isUnit_iff line 64
  11. lemma OAI.SiegelZeros.W58.uniformizer_denominators_units line 73
  12. def OAI.SiegelZeros.W58.uniformizerLocalMap line 78
  13. lemma OAI.SiegelZeros.W58.uniformizerLocalMap_algebraMap line 82
  14. lemma OAI.SiegelZeros.W58.uniformizerLocalMap_injective line 87
  15. lemma OAI.SiegelZeros.W58.uniformizerLocalMap_maximalIdeal line 107
  16. lemma OAI.SiegelZeros.W58.uniformizerLocalMap_isLocalHom line 120
  17. abbrev OAI.SiegelZeros.W58.uniformizerLocalAlgebra line 125
  18. lemma OAI.SiegelZeros.W58.uniformizerLocalAlgebra_flat line 128
  19. lemma OAI.SiegelZeros.W58.formallySmooth_of_essFiniteType_flat_smoothFiber line 140
  20. lemma OAI.SiegelZeros.W58.formallySmooth_of_flat_map_maximalIdeal line 152
  21. theorem OAI.SiegelZeros.W58.dvr_formallySmooth_of_essFiniteType line 187