OAI/AlgebraicGeometry/AbhyankarSathaye/LinearPresentation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The intermediate linear presentation

The relation h * G - y * U = x has parameter α * U + β * G. The remaining compatible equations generate the principal ideal (W - W₀).

  1. def OAI.AbhyankarSathaye.LinearPresentation.relation line 19
  2. def OAI.AbhyankarSathaye.LinearPresentation.ideal line 20
  3. abbrev OAI.AbhyankarSathaye.LinearPresentation.A line 21
  4. def OAI.AbhyankarSathaye.LinearPresentation.qmap line 22
  5. def OAI.AbhyankarSathaye.LinearPresentation.qvar line 24
  6. def OAI.AbhyankarSathaye.LinearPresentation.coeff line 25
  7. theorem OAI.AbhyankarSathaye.LinearPresentation.linear_relation line 27
  8. def OAI.AbhyankarSathaye.LinearPresentation.values line 34
  9. def OAI.AbhyankarSathaye.LinearPresentation.forward line 37
  10. theorem OAI.AbhyankarSathaye.LinearPresentation.forward_qvar line 54
  11. def OAI.AbhyankarSathaye.LinearPresentation.backward line 59
  12. theorem OAI.AbhyankarSathaye.LinearPresentation.forward_backward line 62
  13. theorem OAI.AbhyankarSathaye.LinearPresentation.backward_forward line 72
  14. def OAI.AbhyankarSathaye.LinearPresentation.equivalence line 91
  15. def OAI.AbhyankarSathaye.LinearPresentation.a line 95
  16. def OAI.AbhyankarSathaye.LinearPresentation.b line 96
  17. def OAI.AbhyankarSathaye.LinearPresentation.r line 98
  18. def OAI.AbhyankarSathaye.LinearPresentation.q line 99
  19. def OAI.AbhyankarSathaye.LinearPresentation.W0 line 100
  20. theorem OAI.AbhyankarSathaye.LinearPresentation.compatible line 102
  21. theorem OAI.AbhyankarSathaye.LinearPresentation.bezout_squared line 108
  22. theorem OAI.AbhyankarSathaye.LinearPresentation.W_ideal line 114