OAI/NumberTheory/SiegelZeros/Intersection/DivisorSmoothness.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.NormalizedProjectiveTorus line 15
  2. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorus_integral line 18
  3. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorusToBase line 21
  4. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorus_proper line 25
  5. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorus_locallyNoetherian line 28
  6. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorus_stalk_integrallyClosed line 32
  7. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedProjectiveTorusFunctionFieldEquiv line 36
  8. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.compactifiedTorusCoordinate line 41
  9. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.compactifiedTorusCoordinate_identification line 45
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.compactifiedTorusCoordinate_ne_zero line 50
  11. abbrev OAI.SiegelZeros.W58.ProjectiveDivisorStalk line 66
  12. theorem OAI.SiegelZeros.W58.projective_divisor_stalk_dvr line 69
  13. theorem OAI.SiegelZeros.W58.projective_divisor_stalkMap_essFiniteType line 75
  14. theorem OAI.SiegelZeros.W58.projective_divisor_residueMap_essFiniteType line 79
  15. theorem OAI.SiegelZeros.W58.projective_divisor_residueMap_formallySmooth line 85