OAI/NumberTheory/Jacobsthal/Siegel/LogarithmicForm.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.scheme_coordinates_constant_of_log_form line 32
  2. theorem OAI.Erdos970.WeightedTorusJets.logarithmic_relation_map_algHom line 57
  3. theorem OAI.Erdos970.WeightedTorusJets.coordinates_constant_of_log_form_via_normal_model line 82
  4. theorem OAI.Erdos970.WeightedTorusJets.laurent_range_mem_intermediateField line 116
  5. theorem OAI.Erdos970.WeightedTorusJets.laurent_fraction_adjoin_coordinates line 140
  6. theorem OAI.Erdos970.WeightedTorusJets.laurent_quotient_exists_nonconstant_coordinate line 159
  7. theorem OAI.Erdos970.WeightedTorusJets.derivation_laurent_fraction_eq_zero line 185
  8. theorem OAI.Erdos970.WeightedTorusJets.laurent_finiteType line 206
  9. def OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicForm line 221
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicForm_eq_zero_iff line 225
  11. def OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicTangentMap line 236
  12. def OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicLinearForm line 242
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicLinearForm_apply line 245
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicForm_ne_zero_iff_tangent_not_le line 249
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicForm_ne_zero_on_torus_subvariety_of_normal_model line 275
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicForm_ne_zero_on_torus_subvariety line 313
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_normal_image_of_not_le line 343
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicHyperplane_normal_rank_at_point line 358
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicTangentMap_injective_laurent_quotient line 387
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicHyperplane_generic_normal_rank_eq_codim line 412
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmic_form_lemma_exact line 443