OAI/Geometry/SurfaceImmersion/Correction/MixedPolynomialLocality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mixed variations only use the germs of their four input fields.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.eval_eq_of_eventuallyEq line 11
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateQuadraticPolynomial_eq_of_eventuallyEq line 27