OAI/NumberTheory/SiegelZeros/EntireFunctions/LogarithmicForm.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.scheme_coordinates_constant_of_log_form line 31
  2. theorem OAI.SiegelZeros.WeightedTorusJets.logarithmic_relation_map_algHom line 56
  3. theorem OAI.SiegelZeros.WeightedTorusJets.coordinates_constant_of_log_form_via_normal_model line 81
  4. theorem OAI.SiegelZeros.WeightedTorusJets.laurent_range_mem_intermediateField line 115
  5. theorem OAI.SiegelZeros.WeightedTorusJets.laurent_fraction_adjoin_coordinates line 139
  6. theorem OAI.SiegelZeros.WeightedTorusJets.laurent_quotient_exists_nonconstant_coordinate line 158
  7. theorem OAI.SiegelZeros.WeightedTorusJets.derivation_laurent_fraction_eq_zero line 184
  8. theorem OAI.SiegelZeros.WeightedTorusJets.laurent_finiteType line 205
  9. def OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicForm line 220
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicForm_eq_zero_iff line 224
  11. def OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicTangentMap line 235
  12. def OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicLinearForm line 241
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicLinearForm_apply line 244
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicForm_ne_zero_iff_tangent_not_le line 248
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicForm_ne_zero_on_torus_subvariety_of_normal_model line 274
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicForm_ne_zero_on_torus_subvariety line 312
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_normal_image_of_not_le line 342
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicHyperplane_normal_rank_at_point line 357
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicTangentMap_injective_laurent_quotient line 386
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicHyperplane_generic_normal_rank_eq_codim line 411
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmic_form_lemma_exact line 442