OAI/NumberTheory/SiegelZeros/Structure/CanonicalDivisorScalars.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.scalarToStalk line 19
  2. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.schemeStalkAlgebra line 24
  3. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.schemeFunctionFieldAlgebra line 28
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.scalarToStalk_stalkCongr line 32
  5. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.scalarToStalk_stalkMap line 39
  6. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.scalarToStalk_stalkClosedPointTo line 48
  7. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericPointMorphism_scalars line 63
  8. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalizationFunctionFieldEquiv_scalars line 76
  9. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalizationFunctionFieldAlgEquiv line 92
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.imageFunctionFieldEquiv_scalars line 102
  11. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.imageFunctionFieldAlgEquiv line 115
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affine_scalarToStalk line 131
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusSubvarietyEmbedding_toBase line 147
  14. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusFunctionFieldAlgebra line 155
  15. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.compactifiedFunctionFieldAlgebra line 160
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorusFunctionFieldEquiv_scalars line 164
  17. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorusFunctionFieldAlgEquiv line 180
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorusFunctionFieldAlgEquiv_coordinate line 190
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.scalarToStalk_via_chart line 201
  20. theorem OAI.SiegelZeros.W58.scalarToStalk_base_identity line 238
  21. theorem OAI.SiegelZeros.W58.scalarToStalk_structural_factorization line 244
  22. theorem OAI.SiegelZeros.W58.canonical_schemeStalk_essFiniteType line 251
  23. theorem OAI.SiegelZeros.W58.canonical_schemeStalk_residue_formallySmooth line 265
  24. theorem OAI.SiegelZeros.W58.projective_divisor_stalk_essFiniteType line 280
  25. theorem OAI.SiegelZeros.W58.projective_divisor_residue_formallySmooth line 285