OAI/Geometry/HypersurfaceGerms/Germs.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Reduced isolated holomorphic germs with specified ordinary orders.

  1. abbrev OAI.AmbientMultiplicity.C4 line 12
  2. def OAI.AmbientMultiplicity.ReducedAtZero line 15
  3. def OAI.AmbientMultiplicity.HasOrderAtZero line 20
  4. def OAI.AmbientMultiplicity.IsolatedCriticalAtZero line 25
  5. def OAI.AmbientMultiplicity.AmbientPairEquivalent line 30
  6. def OAI.AmbientMultiplicity.MainStatement line 36
  7. def OAI.AmbientMultiplicity.planeH line 50
  8. def OAI.AmbientMultiplicity.planeHX line 51
  9. def OAI.AmbientMultiplicity.planeHT line 52
  10. def OAI.AmbientMultiplicity.planeQ1 line 54
  11. def OAI.AmbientMultiplicity.planeQ2 line 55
  12. def OAI.AmbientMultiplicity.graphPhi line 56
  13. def OAI.AmbientMultiplicity.graphPsi line 57
  14. theorem OAI.AmbientMultiplicity.planeH_expansion line 61
  15. theorem OAI.AmbientMultiplicity.gradient_elimination line 67
  16. theorem OAI.AmbientMultiplicity.base_gradient_zero_iff line 74
  17. lemma OAI.AmbientMultiplicity.critical_origin_of_order line 91
  18. theorem OAI.AmbientMultiplicity.exact_source_germs line 99