OAI/Geometry/HypersurfaceGerms/Jets.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Derivative-order calculus and vanishing jets.

  1. def OAI.AmbientMultiplicity.Jets.Vanishing line 13
  2. lemma OAI.AmbientMultiplicity.Jets.analytic_neighborhood line 16
  3. lemma OAI.AmbientMultiplicity.Jets.Vanishing.analytic line 24
  4. lemma OAI.AmbientMultiplicity.Jets.Vanishing.zero line 25
  5. lemma OAI.AmbientMultiplicity.Jets.Vanishing.mono line 26
  6. lemma OAI.AmbientMultiplicity.Jets.Vanishing.one line 28
  7. lemma OAI.AmbientMultiplicity.Jets.Vanishing.eq_zero line 35
  8. lemma OAI.AmbientMultiplicity.Jets.Vanishing.congr line 38
  9. lemma OAI.AmbientMultiplicity.Jets.Vanishing.add line 42
  10. lemma OAI.AmbientMultiplicity.Jets.Vanishing.sub line 48
  11. lemma OAI.AmbientMultiplicity.Jets.Vanishing.mul line 55
  12. lemma OAI.AmbientMultiplicity.Jets.Vanishing.const_mul line 78
  13. lemma OAI.AmbientMultiplicity.Jets.Vanishing.mul_const line 80
  14. lemma OAI.AmbientMultiplicity.Jets.Vanishing.pow line 82
  15. lemma OAI.AmbientMultiplicity.Jets.iteratedFDeriv_comp_linear line 92
  16. lemma OAI.AmbientMultiplicity.Jets.derivative_eq_of_remainder line 108
  17. lemma OAI.AmbientMultiplicity.Jets.nonzero_derivative_of_line line 117
  18. lemma OAI.AmbientMultiplicity.Jets.Vanishing.gradient_zero line 132
  19. lemma OAI.AmbientMultiplicity.Jets.order_of_remainder line 139