OAI/Geometry/QuadricBundles/Embedding.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuadricCounterexample.AlgebraicRankTwoBundle.dualTransition_self line 16
  2. lemma OAI.QuadricCounterexample.AlgebraicRankTwoBundle.dualTransition_mul line 20
  3. lemma OAI.QuadricCounterexample.AlgebraicRankTwoBundle.dualTransition_nonzero line 25
  4. lemma OAI.QuadricCounterexample.sectionVector_compatible line 34
  5. structure OAI.QuadricCounterexample.StandardBundleCover line 41
  6. def OAI.QuadricCounterexample.StandardBundleCover.chartIndex line 47
  7. lemma OAI.QuadricCounterexample.StandardBundleCover.chartIndex_lt line 48
  8. lemma OAI.QuadricCounterexample.StandardBundleCover.chartIndex_chart line 49
  9. lemma OAI.QuadricCounterexample.StandardBundleCover.chartIndex_mem line 50
  10. structure OAI.QuadricCounterexample.SegreSectionSystem line 55
  11. lemma OAI.QuadricCounterexample.SegreSectionSystem.nonzero line 64
  12. lemma OAI.QuadricCounterexample.SegreSectionSystem.pivot_domain line 68
  13. lemma OAI.QuadricCounterexample.SegreSectionSystem.localize_pivot line 80
  14. lemma OAI.QuadricCounterexample.SegreSectionSystem.pivot_coordinates line 94
  15. lemma OAI.QuadricCounterexample.SegreSectionSystem.pivot_recovery line 100
  16. lemma OAI.QuadricCounterexample.SegreSectionSystem.exists_pivot line 106
  17. lemma OAI.QuadricCounterexample.SegreSectionSystem.injective line 117
  18. lemma OAI.QuadricCounterexample.lineFactor_add line 161
  19. lemma OAI.QuadricCounterexample.lineFactor_diagonal line 165
  20. lemma OAI.QuadricCounterexample.eval_polynomial_smul_vector line 167
  21. lemma OAI.QuadricCounterexample.eval_polynomial_smul_coeff line 176
  22. lemma OAI.QuadricCounterexample.polynomial_eval_dot line 182
  23. lemma OAI.QuadricCounterexample.EqualizerData.powerTwist_cover line 192
  24. def OAI.QuadricCounterexample.EqualizerData.fullSymmetricCoefficient line 201
  25. lemma OAI.QuadricCounterexample.EqualizerData.fullSymmetricCoefficient_value line 204
  26. lemma OAI.QuadricCounterexample.EqualizerData.fullSymmetricCoefficient_compatible line 213
  27. lemma OAI.QuadricCounterexample.EqualizerData.powerTwist_transition line 227
  28. def OAI.QuadricCounterexample.EqualizerData.ampleSection line 242
  29. lemma OAI.QuadricCounterexample.EqualizerData.ampleSection_value line 274
  30. def OAI.QuadricCounterexample.EqualizerData.ampleSystem line 284
  31. lemma OAI.QuadricCounterexample.SegreSectionSystem.cone_algebraic line 306
  32. def OAI.QuadricCounterexample.SegreSectionSystem.inverseNumerator line 323
  33. def OAI.QuadricCounterexample.SegreSectionSystem.inverseDenominator line 327
  34. lemma OAI.QuadricCounterexample.SegreSectionSystem.recoveryPolynomial_value line 330
  35. lemma OAI.QuadricCounterexample.SegreSectionSystem.inverseDenominator_value line 338
  36. lemma OAI.QuadricCounterexample.SegreSectionSystem.inverseDenominator_nonzero line 346
  37. lemma OAI.QuadricCounterexample.SegreSectionSystem.inverseFormula line 357
  38. lemma OAI.QuadricCounterexample.SegreSectionSystem.local_inverse line 376
  39. theorem OAI.QuadricCounterexample.SegreSectionSystem.closedEmbedding line 414