OAI/Geometry/SplitTangent/CurveHomogeneousSections.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Curve Homogeneous Sections.

  1. lemma OAI.SplitTangent.RationalCurveFrames.multiplier_holomorphicAt line 20
  2. lemma OAI.SplitTangent.RationalCurveFrames.multiplier_formula line 27
  3. lemma OAI.SplitTangent.RationalCurveFrames.frame_transition_eventually line 36
  4. def OAI.SplitTangent.RationalCurveFrames.ambientTransition line 49
  5. abbrev OAI.SplitTangent.RationalCurveFrames.HomogeneousTuple line 59
  6. def OAI.SplitTangent.RationalCurveFrames.sections line 63