OAI/Geometry/SplitTangent/Basic.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Basic.

  1. structure OAI.SplitTangent.ComplexManifold line 15

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:15 (same declaration text).

  2. abbrev OAI.SplitTangent.Model line 28

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:28 (same declaration text).

  3. abbrev OAI.SplitTangent.ModelWithCorners line 29

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:29 (same declaration text).

  4. abbrev OAI.SplitTangent.Tangent line 30

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:30 (same declaration text).

  5. abbrev OAI.SplitTangent.ProjectiveSpace line 33

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:33 (same declaration text).

  6. def OAI.SplitTangent.projectiveCoordinates line 37

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:37 (same declaration text).

  7. structure OAI.SplitTangent.ProjectiveEmbedding line 43

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:43 (same declaration text).

  8. def OAI.SplitTangent.IsProjective line 55
  9. structure OAI.SplitTangent.RationalCurve line 59

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:55 (same declaration text).

  10. def OAI.SplitTangent.RationalCurve.value line 66

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:62 (same declaration text).

  11. abbrev OAI.SplitTangent.PairPolynomial line 70

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:66 (same declaration text).

  12. def OAI.SplitTangent.Bihomogeneous line 73

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:69 (same declaration text).

  13. def OAI.SplitTangent.pairEval line 78

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:74 (same declaration text).

  14. def OAI.SplitTangent.IsZariskiOpenPair line 86

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:82 (same declaration text).

  15. def OAI.SplitTangent.RationallyConnected line 94

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:90 (same declaration text).

  16. structure OAI.SplitTangent.TangentSplitting line 101

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:97 (same declaration text).

  17. def OAI.SplitTangent.TangentSplitting.first line 112

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:108 (same declaration text).

  18. def OAI.SplitTangent.TangentSplitting.second line 115

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:111 (same declaration text).

  19. def OAI.SplitTangent.HolomorphicSectionOn line 120

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:116 (same declaration text).

  20. def OAI.SplitTangent.Integrable line 126

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:122 (same declaration text).

  21. def OAI.SplitTangent.HasCompatibleProjectiveProduct line 134
  22. def OAI.SplitTangent.MainStatement line 147