OAI/AlgebraicGeometry/AbhyankarSathaye/Reconstruction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Mutually inverse polynomial formulas

The parameter T = α * U + β * (V + U * W) and the formulas inverseU, inverseV, and inverseW reconstruct each other over arbitrary commutative rings.

  1. def OAI.AbhyankarSathaye.inverseU line 16
  2. def OAI.AbhyankarSathaye.inverseG line 17
  3. def OAI.AbhyankarSathaye.inverseW line 18
  4. def OAI.AbhyankarSathaye.inverseV line 20
  5. def OAI.AbhyankarSathaye.parameter line 21
  6. theorem OAI.AbhyankarSathaye.inverse_relations line 23
  7. theorem OAI.AbhyankarSathaye.inverse_parameter line 41
  8. theorem OAI.AbhyankarSathaye.original_reconstruction line 52
  9. theorem OAI.AbhyankarSathaye.map_inverseU line 81
  10. theorem OAI.AbhyankarSathaye.map_inverseG line 83
  11. theorem OAI.AbhyankarSathaye.map_inverseW line 85
  12. theorem OAI.AbhyankarSathaye.map_inverseV line 88
  13. theorem OAI.AbhyankarSathaye.map_parameter line 90