OAI/AlgebraicGeometry/AbhyankarSathaye/LiftingIdentities.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Linear equations for the lifting construction

The substitution G = V + U * W makes the equations linear in W. A Bézout relation gives existence and uniqueness without cancellation.

  1. theorem OAI.AbhyankarSathaye.substitute_S line 16
  2. theorem OAI.AbhyankarSathaye.compatibility_identity line 22
  3. theorem OAI.AbhyankarSathaye.compatibility line 26
  4. theorem OAI.AbhyankarSathaye.squared_bezout line 32
  5. theorem OAI.AbhyankarSathaye.solve_h line 38
  6. theorem OAI.AbhyankarSathaye.solve_c line 45
  7. theorem OAI.AbhyankarSathaye.solve_unique line 52
  8. theorem OAI.AbhyankarSathaye.linear_parameter_relation line 59
  9. theorem OAI.AbhyankarSathaye.linear_parameter_inverse line 65
  10. theorem OAI.AbhyankarSathaye.recover_U line 71
  11. theorem OAI.AbhyankarSathaye.recover_G line 78
  12. theorem OAI.AbhyankarSathaye.original_to_linear line 85
  13. theorem OAI.AbhyankarSathaye.linear_to_original line 103