OAI/NumberTheory/SiegelZeros/Differentials/UnconditionalGlobalLogform.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.logform_zero_transport line 24
  2. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.independent_logform_zero_forces_equal_orders line 49
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.independent_logform_zero_forces_local_regularity line 73
  4. def OAI.SiegelZeros.WeightedTorusJets.NormalExactness.residueLogForm line 104
  5. def OAI.SiegelZeros.WeightedTorusJets.NormalExactness.logFormOnDerivations line 109
  6. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.tangent_logForm_pairing line 120
  7. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.exists_tangent_not_annihilated line 130
  8. def OAI.SiegelZeros.WeightedTorusJets.NormalExactness.logarithmicNormalMap line 145
  9. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.logarithmicNormalMap_surjective line 150
  10. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.select_actual_logarithmic_normals line 168
  11. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.DivisorFormalSmoothness line 206
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.compactified_zero_logform_coordinates_constant line 212
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.torus_functionField_logform_ne_zero line 244
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.residueLogForm_zero_scalar_coefficients line 266
  15. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.torus_residueLogForm_ne_zero line 284
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.actual_projective_divisor_formallySmooth line 328
  17. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.actual_divisorFormalSmoothness line 339
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.compactified_zero_logform_coordinates_constant_unconditional line 343
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.torus_functionField_logform_ne_zero_unconditional line 351
  20. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W14.torus_residueLogForm_ne_zero_unconditional line 360