OAI/NumberTheory/SiegelZeros/LocalAlgebra/GlobalStalkExtension.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.globalExtension_top_nonempty line 21
  2. lemma OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.germToFunctionField_restrict line 24
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.global_preimage_of_open_cover line 29
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affine_integrallyClosed_of_stalks line 68
  5. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affine_preimage_of_heightOne line 85
  6. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.global_preimage_of_affine_heightOne line 108
  7. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.actualStalk_isFractionRing line 138
  8. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affine_fraction_of_dimensionOne_stalks line 141
  9. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.global_preimage_of_dimensionOne_stalks line 175
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.schemeScalarTower_stalk_functionField line 194
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.scalarToFunctionField_constantSection line 213