OAI/NumberTheory/SiegelZeros/Determinants/GenericNormalizationFinite.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.finite_normalization_of_finite_normal_base line 22
  2. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.finite_normalization_of_finiteType line 44
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.finite_integralClosure_of_finiteType line 55
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineNormalizationMap_finite_of_finiteType line 63
  5. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineNormalizationMap_proper_of_finiteType line 70
  6. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericPointMorphism line 86
  7. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.GenericNormalization line 90
  8. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalizationMap line 93
  9. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalization_integral line 96
  10. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalizationMap_integral line 98
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericPointMorphism_preimage line 102
  12. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericSourceSectionsIso line 117
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalization_chart_integrallyClosed line 125
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalization_stalk_integrallyClosed line 143
  15. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.toGenericNormalization_closedPoint line 171
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.toGenericNormalization_stalk_surjective line 188
  17. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalizationFunctionFieldEquiv line 204
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericSourceSectionsIso_app line 222
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericSourceSections_isFractionRing line 238
  20. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalizationMap_finite line 258
  21. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.genericNormalization_proper line 298