OAI/Geometry/QuadricBundles/BinaryForms.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuadricCounterexample.BinaryForms.Form line 15
  2. abbrev OAI.QuadricCounterexample.BinaryForms.Poly line 16
  3. def OAI.QuadricCounterexample.BinaryForms.exponent line 18
  4. lemma OAI.QuadricCounterexample.BinaryForms.exponent_zero line 20
  5. lemma OAI.QuadricCounterexample.BinaryForms.exponent_one line 22
  6. lemma OAI.QuadricCounterexample.BinaryForms.exponent_injective line 24
  7. lemma OAI.QuadricCounterexample.BinaryForms.degree_binary line 28
  8. lemma OAI.QuadricCounterexample.BinaryForms.exponent_degree line 30
  9. lemma OAI.QuadricCounterexample.BinaryForms.exponent_of_degree line 33
  10. def OAI.QuadricCounterexample.BinaryForms.polynomial line 43
  11. def OAI.QuadricCounterexample.BinaryForms.coefficients line 45
  12. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_homogeneous line 48
  13. lemma OAI.QuadricCounterexample.BinaryForms.coefficients_polynomial line 53
  14. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_coefficients line 62
  15. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_injective line 69
  16. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_add line 72
  17. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_smul line 75
  18. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_zero line 78
  19. lemma OAI.QuadricCounterexample.BinaryForms.coefficients_add line 79
  20. lemma OAI.QuadricCounterexample.BinaryForms.coefficients_smul line 81
  21. def OAI.QuadricCounterexample.BinaryForms.equivHomogeneous line 84
  22. lemma OAI.QuadricCounterexample.BinaryForms.eval_polynomial line 92
  23. lemma OAI.QuadricCounterexample.BinaryForms.coefficients_monomial_diff line 101
  24. lemma OAI.QuadricCounterexample.BinaryForms.homogeneous_projection line 109
  25. def OAI.QuadricCounterexample.BinaryForms.kernelForm line 139
  26. def OAI.QuadricCounterexample.BinaryForms.liftForm line 140
  27. lemma OAI.QuadricCounterexample.BinaryForms.kernelForm_homogeneous line 141
  28. lemma OAI.QuadricCounterexample.BinaryForms.liftForm_homogeneous line 143
  29. lemma OAI.QuadricCounterexample.BinaryForms.eval_kernelForm line 145
  30. lemma OAI.QuadricCounterexample.BinaryForms.eval_liftForm line 147
  31. lemma OAI.QuadricCounterexample.BinaryForms.kernelForm_ne_zero line 149
  32. def OAI.QuadricCounterexample.BinaryForms.adaptedPolynomials line 158
  33. lemma OAI.QuadricCounterexample.BinaryForms.adaptedPolynomials_homogeneous line 163
  34. lemma OAI.QuadricCounterexample.BinaryForms.sum_snoc_two line 176
  35. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_sum_smul line 184
  36. lemma OAI.QuadricCounterexample.BinaryForms.eval_sum_smul line 192
  37. lemma OAI.QuadricCounterexample.BinaryForms.adaptedPolynomials_independent line 196
  38. def OAI.QuadricCounterexample.BinaryForms.adaptedMatrix line 238
  39. lemma OAI.QuadricCounterexample.BinaryForms.adaptedMatrix_columns line 240
  40. lemma OAI.QuadricCounterexample.BinaryForms.adaptedMatrix_independent line 243
  41. lemma OAI.QuadricCounterexample.BinaryForms.adaptedMatrix_isUnit line 253
  42. def OAI.QuadricCounterexample.BinaryForms.substitute line 266
  43. lemma OAI.QuadricCounterexample.BinaryForms.substitute_X line 268
  44. lemma OAI.QuadricCounterexample.BinaryForms.substitute_C line 270
  45. lemma OAI.QuadricCounterexample.BinaryForms.substitute_comp line 272
  46. lemma OAI.QuadricCounterexample.BinaryForms.substitute_one line 286
  47. lemma OAI.QuadricCounterexample.BinaryForms.substitute_homogeneous line 292
  48. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_linearCombination line 313
  49. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_mulVec line 321
  50. def OAI.QuadricCounterexample.BinaryForms.symmetricMatrix line 332
  51. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_symmetricMatrix_col line 334
  52. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_symmetricMatrix line 337
  53. lemma OAI.QuadricCounterexample.BinaryForms.symmetricMatrix_mul line 347
  54. lemma OAI.QuadricCounterexample.BinaryForms.symmetricMatrix_one line 354
  55. lemma OAI.QuadricCounterexample.BinaryForms.eval_substitute line 359
  56. lemma OAI.QuadricCounterexample.BinaryForms.adaptedMatrix_det_unit line 374
  57. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_adapted_mulVec line 378
  58. lemma OAI.QuadricCounterexample.BinaryForms.adapted_combination_succ line 384
  59. lemma OAI.QuadricCounterexample.BinaryForms.eval_adapted_combination line 394
  60. def OAI.QuadricCounterexample.BinaryForms.adaptedCoordinates line 401
  61. lemma OAI.QuadricCounterexample.BinaryForms.adaptedCoordinates_smul line 403
  62. lemma OAI.QuadricCounterexample.BinaryForms.polynomial_adaptedCoordinates line 408
  63. lemma OAI.QuadricCounterexample.BinaryForms.adaptedCoordinates_combination line 413
  64. lemma OAI.QuadricCounterexample.BinaryForms.adaptedCoordinates_last line 418
  65. lemma OAI.QuadricCounterexample.BinaryForms.adaptedCoordinates_residual line 424
  66. lemma OAI.QuadricCounterexample.BinaryForms.adaptedCoordinates_penultimate line 435
  67. structure OAI.QuadricCounterexample.BinaryForms.FlagFrame line 462
  68. def OAI.QuadricCounterexample.BinaryForms.FlagFrame.matrix line 469
  69. def OAI.QuadricCounterexample.BinaryForms.FlagFrame.column line 470
  70. def OAI.QuadricCounterexample.BinaryForms.FlagFrame.coords line 471
  71. lemma OAI.QuadricCounterexample.BinaryForms.FlagFrame.det_unit line 472
  72. structure OAI.QuadricCounterexample.BinaryForms.FlagChange line 476
  73. def OAI.QuadricCounterexample.BinaryForms.FlagChange.matrix line 488
  74. lemma OAI.QuadricCounterexample.BinaryForms.FlagChange.matrix_col line 490
  75. lemma OAI.QuadricCounterexample.BinaryForms.FlagChange.matrix_entry line 502
  76. lemma OAI.QuadricCounterexample.BinaryForms.FlagChange.matrix_column_residual line 505
  77. lemma OAI.QuadricCounterexample.BinaryForms.FlagChange.matrix_pen_last line 521
  78. lemma OAI.QuadricCounterexample.BinaryForms.FlagChange.matrix_pen_diag line 532
  79. lemma OAI.QuadricCounterexample.BinaryForms.FlagChange.matrix_last_diag line 544
  80. def OAI.QuadricCounterexample.BinaryForms.FlagChange.graded line 553
  81. lemma OAI.QuadricCounterexample.BinaryForms.FlagChange.matrix_zero line 557
  82. lemma OAI.QuadricCounterexample.BinaryForms.FlagChange.triangular_diagonal line 569