OAI/Geometry/QuadricBundles/RegularMatrices.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadricCounterexample.regularFunctionRing line 14
  2. def OAI.QuadricCounterexample.regularEval line 22
  3. lemma OAI.QuadricCounterexample.UniformlyRegularOn.matrix_det line 29
  4. lemma OAI.QuadricCounterexample.UniformlyRegularOn.matrix_adjugate line 38
  5. lemma OAI.QuadricCounterexample.UniformlyRegularOn.matrix_inv line 47
  6. lemma OAI.QuadricCounterexample.UniformlyRegularOn.matrix_mul line 55
  7. def OAI.QuadricCounterexample.BinaryForms.RegularFamily line 64
  8. lemma OAI.QuadricCounterexample.BinaryForms.RegularFamily.const line 66
  9. lemma OAI.QuadricCounterexample.BinaryForms.RegularFamily.C line 68
  10. lemma OAI.QuadricCounterexample.BinaryForms.RegularFamily.add line 74
  11. lemma OAI.QuadricCounterexample.BinaryForms.RegularFamily.sub line 78
  12. lemma OAI.QuadricCounterexample.BinaryForms.RegularFamily.mul line 82
  13. lemma OAI.QuadricCounterexample.BinaryForms.RegularFamily.pow line 87
  14. lemma OAI.QuadricCounterexample.BinaryForms.RegularFamily.fintype_sum line 92
  15. lemma OAI.QuadricCounterexample.BinaryForms.substitute_regular line 97
  16. lemma OAI.QuadricCounterexample.BinaryForms.symmetricMatrix_regular line 106
  17. lemma OAI.QuadricCounterexample.BinaryForms.adaptedPolynomials_regular line 110
  18. lemma OAI.QuadricCounterexample.BinaryForms.adaptedMatrix_regular line 128
  19. lemma OAI.QuadricCounterexample.polynomial_bezout line 140
  20. def OAI.QuadricCounterexample.EqualizerData.bezoutU line 160
  21. def OAI.QuadricCounterexample.EqualizerData.bezoutV line 161
  22. lemma OAI.QuadricCounterexample.EqualizerData.bezout_spec line 163
  23. lemma OAI.QuadricCounterexample.EqualizerData.bezout_eval line 165
  24. def OAI.QuadricCounterexample.EqualizerData.kernelFactor line 180
  25. lemma OAI.QuadricCounterexample.EqualizerData.kernelFactor_regular line 182
  26. lemma OAI.QuadricCounterexample.EqualizerData.kernelFactor_divisor line 186
  27. lemma OAI.QuadricCounterexample.EqualizerData.bottomFactor_divisor line 192
  28. lemma OAI.QuadricCounterexample.EqualizerData.kernelFactor_bottomFactor line 198
  29. lemma OAI.QuadricCounterexample.EqualizerData.kernel_coordinates line 205
  30. lemma OAI.QuadricCounterexample.EqualizerData.substitute_kernel line 228
  31. lemma OAI.QuadricCounterexample.EqualizerData.substitute_f line 242
  32. lemma OAI.QuadricCounterexample.EqualizerData.substitute_e_projection line 246
  33. lemma OAI.QuadricCounterexample.EqualizerData.quotient_covector line 250
  34. lemma OAI.QuadricCounterexample.EqualizerData.substitute_lift_quotient line 262