OAI/Geometry/QuadricBundles/TriangularSections.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuadricCounterexample.UniformlyRegularOn.finset_sum line 14
  2. lemma OAI.QuadricCounterexample.UniformlyRegularOn.fintype_sum line 24
  3. lemma OAI.QuadricCounterexample.LaurentCech.scalarFactor_mul_one_overlap line 31
  4. lemma OAI.QuadricCounterexample.LaurentCech.lineFactor_mul_one_overlap line 34
  5. lemma OAI.QuadricCounterexample.LaurentCech.lineFactor_self line 45
  6. def OAI.QuadricCounterexample.LaurentCech.lineGenerator line 48
  7. lemma OAI.QuadricCounterexample.LaurentCech.eval_lineGenerator line 50
  8. lemma OAI.QuadricCounterexample.LaurentCech.lineGenerator_compatible line 54
  9. structure OAI.QuadricCounterexample.TriangularCechBundle line 64
  10. def OAI.QuadricCounterexample.TriangularCechBundle.polynomialValue line 76
  11. def OAI.QuadricCounterexample.TriangularCechBundle.delta line 79
  12. lemma OAI.QuadricCounterexample.TriangularCechBundle.delta_regular line 81
  13. lemma OAI.QuadricCounterexample.TriangularCechBundle.delta_cocycle line 89
  14. lemma OAI.QuadricCounterexample.TriangularCechBundle.delta_add line 95
  15. lemma OAI.QuadricCounterexample.TriangularCechBundle.delta_zero line 102
  16. lemma OAI.QuadricCounterexample.TriangularCechBundle.row_of_high_zero line 106
  17. structure OAI.QuadricCounterexample.TriangularCechBundle.Cocycle line 118
  18. def OAI.QuadricCounterexample.TriangularCechBundle.coboundary line 124
  19. def OAI.QuadricCounterexample.TriangularCechBundle.Cocycle.sub line 129
  20. theorem OAI.QuadricCounterexample.TriangularCechBundle.solve_upTo line 138
  21. theorem OAI.QuadricCounterexample.TriangularCechBundle.solve line 197
  22. structure OAI.QuadricCounterexample.TriangularCechBundle.Section line 212
  23. lemma OAI.QuadricCounterexample.TriangularCechBundle.delta_sub line 218
  24. theorem OAI.QuadricCounterexample.TriangularCechBundle.exists_generator line 226
  25. def OAI.QuadricCounterexample.TriangularCechBundle.generator line 262
  26. lemma OAI.QuadricCounterexample.TriangularCechBundle.generator_high line 263
  27. lemma OAI.QuadricCounterexample.TriangularCechBundle.generator_diagonal line 265
  28. def OAI.QuadricCounterexample.TriangularCechBundle.generatorMatrix line 269
  29. lemma OAI.QuadricCounterexample.TriangularCechBundle.generatorMatrix_self_det line 271
  30. lemma OAI.QuadricCounterexample.TriangularCechBundle.generatorMatrix_self_isUnit line 279
  31. theorem OAI.QuadricCounterexample.TriangularCechBundle.generated line 283