OAI/Geometry/QuadricBundles/ProjectiveEquations.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadricCounterexample.BinaryForms.veronese line 14
  2. lemma OAI.QuadricCounterexample.BinaryForms.veronese_zero line 15
  3. lemma OAI.QuadricCounterexample.BinaryForms.veronese_last line 16
  4. lemma OAI.QuadricCounterexample.BinaryForms.veronese_nonzero line 17
  5. def OAI.QuadricCounterexample.BinaryForms.veroneseOne line 28
  6. lemma OAI.QuadricCounterexample.BinaryForms.veronese_ratio line 29
  7. def OAI.QuadricCounterexample.BinaryForms.VeroneseRelations line 35
  8. lemma OAI.QuadricCounterexample.BinaryForms.veronese_relations line 38
  9. lemma OAI.QuadricCounterexample.BinaryForms.VeroneseRelations.reconstruct line 63
  10. def OAI.QuadricCounterexample.BinaryForms.veroneseEndpoint line 103
  11. def OAI.QuadricCounterexample.BinaryForms.veroneseAdjacent line 104
  12. lemma OAI.QuadricCounterexample.BinaryForms.veronese_endpoint line 106
  13. lemma OAI.QuadricCounterexample.BinaryForms.veronese_adjacent_ratio line 109
  14. lemma OAI.QuadricCounterexample.BinaryForms.binary_proportional_of_ratio line 123
  15. lemma OAI.QuadricCounterexample.BinaryForms.veronese_projective_injective line 136
  16. def OAI.QuadricCounterexample.flipFirst line 164
  17. def OAI.QuadricCounterexample.flipSecond line 165
  18. def OAI.QuadricCounterexample.segreFactor line 166
  19. lemma OAI.QuadricCounterexample.segreFactor_self line 168
  20. lemma OAI.QuadricCounterexample.segreFactor_flipFirst line 170
  21. lemma OAI.QuadricCounterexample.segreFactor_flipSecond line 175
  22. lemma OAI.QuadricCounterexample.segreFactor_ne_zero_iff line 180
  23. abbrev OAI.QuadricCounterexample.PolynomialGeneration.ProjectiveIndex line 205
  24. def OAI.QuadricCounterexample.PolynomialGeneration.index line 206
  25. def OAI.QuadricCounterexample.PolynomialGeneration.label line 207
  26. lemma OAI.QuadricCounterexample.PolynomialGeneration.label_index line 208
  27. lemma OAI.QuadricCounterexample.PolynomialGeneration.index_label line 209
  28. def OAI.QuadricCounterexample.PolynomialGeneration.stencil line 211
  29. def OAI.QuadricCounterexample.PolynomialGeneration.value line 213
  30. lemma OAI.QuadricCounterexample.PolynomialGeneration.stencil_index line 215
  31. lemma OAI.QuadricCounterexample.PolynomialGeneration.stencil_self line 218
  32. lemma OAI.QuadricCounterexample.PolynomialGeneration.stencil_smul line 221
  33. lemma OAI.QuadricCounterexample.PolynomialGeneration.stencil_nonzero line 226
  34. lemma OAI.QuadricCounterexample.PolynomialGeneration.value_nonzero line 232
  35. def OAI.QuadricCounterexample.PolynomialGeneration.normalize line 235
  36. lemma OAI.QuadricCounterexample.PolynomialGeneration.normalize_smul line 236
  37. lemma OAI.QuadricCounterexample.PolynomialGeneration.normalize_pivot line 240
  38. def OAI.QuadricCounterexample.PolynomialGeneration.patchCoordinates line 243
  39. def OAI.QuadricCounterexample.PolynomialGeneration.block line 245
  40. def OAI.QuadricCounterexample.PolynomialGeneration.patchRecovery line 246
  41. lemma OAI.QuadricCounterexample.PolynomialGeneration.patchCoordinates_stencil line 248
  42. lemma OAI.QuadricCounterexample.PolynomialGeneration.patchRecovery_stencil line 254
  43. lemma OAI.QuadricCounterexample.exists_homogenizeAt line 274
  44. lemma OAI.QuadricCounterexample.projectiveCone_of_patch_equations line 296
  45. lemma OAI.QuadricCounterexample.PolynomialGeneration.normalize_eq_smul line 338
  46. lemma OAI.QuadricCounterexample.PolynomialGeneration.stencil_zero line 342
  47. def OAI.QuadricCounterexample.PolynomialGeneration.liftPatchPolynomial line 346
  48. lemma OAI.QuadricCounterexample.PolynomialGeneration.eval_liftPatchPolynomial line 349
  49. def OAI.QuadricCounterexample.PolynomialGeneration.recoveryPolynomial line 358
  50. lemma OAI.QuadricCounterexample.PolynomialGeneration.eval_recoveryPolynomial line 361
  51. def OAI.QuadricCounterexample.PolynomialGeneration.patchEquations line 366
  52. lemma OAI.QuadricCounterexample.PolynomialGeneration.patchEquations_iff line 375
  53. lemma OAI.QuadricCounterexample.PolynomialGeneration.normalized_value_equations line 388
  54. lemma OAI.QuadricCounterexample.PolynomialGeneration.patchEquations_reconstruct line 397
  55. theorem OAI.QuadricCounterexample.PolynomialGeneration.algebraicCone_of_localization line 413