OAI/Geometry/SplitTangent/ProjectiveHypersurfaces.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Projective Hypersurfaces.

  1. lemma OAI.SplitTangent.LocallyHolomorphicZeroSet.isClosed line 17
  2. def OAI.SplitTangent.ProjectiveEmbedding.homogeneousZeroLocus line 32
  3. lemma OAI.SplitTangent.ProjectiveEmbedding.homogeneous_coordinates_eval line 35
  4. lemma OAI.SplitTangent.ProjectiveEmbedding.homogeneous_coordinates_zero_iff line 41
  5. lemma OAI.SplitTangent.ProjectiveEmbedding.homogeneousZeroLocus_locally_holomorphic line 47
  6. lemma OAI.SplitTangent.ProjectiveEmbedding.homogeneousZeroLocus_isClosed line 64
  7. lemma OAI.SplitTangent.ProjectiveEmbedding.linearFrame_zero_iff line 69
  8. lemma OAI.SplitTangent.ProjectiveEmbedding.linearFrame_denominator_eventually line 76