OAI/Geometry/SplitTangent/PolynomialLeafGerms.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Leaf Germs.

  1. def OAI.SplitTangent.RationalCurveFrames.baseMultiplier line 22
  2. lemma OAI.SplitTangent.RationalCurveFrames.baseMultiplier_holomorphic line 25
  3. lemma OAI.SplitTangent.RationalCurveFrames.baseMultiplier_one line 33
  4. lemma OAI.SplitTangent.RationalCurveFrames.base_frame_eventually line 37
  5. theorem OAI.SplitTangent.RationalCurveFrames.flat_section_coefficients line 61