OAI/AlgebraicGeometry/CommutingDerivations/ParameterBezout.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A relative Bézout identity over an arbitrary commutative ring. The inverse of c is specified by the equation c * d = 1.

  1. def OAI.AbhyankarSathaye.CommutingDerivations.parameterA line 13
  2. def OAI.AbhyankarSathaye.CommutingDerivations.parameterB line 15
  3. theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_bezout_certificate line 18
  4. theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_bezout_unit line 25
  5. theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_shift line 40
  6. theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_recover_s line 46
  7. theorem OAI.AbhyankarSathaye.CommutingDerivations.map_parameterA line 58
  8. theorem OAI.AbhyankarSathaye.CommutingDerivations.map_parameterB line 62