OAI/AlgebraicGeometry/CommutingDerivations/CoefficientInstances.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete Laurent coefficient ring is a characteristic-zero domain. These instances are consequences of its actual localization construction.

  1. instance OAI.AbhyankarSathaye.CommutingDerivations.laurentCoefficients_isDomain line 11
  2. instance OAI.AbhyankarSathaye.CommutingDerivations.laurentCoefficients_charZero line 14