Documentation

Mathlib.RingTheory.Kaehler.Polynomial

The Kaehler differential module of polynomial algebras #

The relative differential module of a polynomial algebra R[σ] is the free module generated by { dx | x ∈ σ }. Also see KaehlerDifferential.mvPolynomialBasis.

Instances For
    noncomputable def KaehlerDifferential.mvPolynomialBasis (R : Type u) [CommRing R] (σ : Type u_1) :

    { dx | x ∈ σ } forms a basis of the relative differential module of a polynomial algebra R[σ].

    Equations
    Instances For
      noncomputable instance instFreeMvPolynomialKaehlerDifferential (R : Type u) [CommRing R] (σ : Type u_1) :
      Equations
      • =
      theorem KaehlerDifferential.polynomial_D_apply (R : Type u) [CommRing R] (P : Polynomial R) :
      (KaehlerDifferential.D R (Polynomial R)) P = Polynomial.derivative P (KaehlerDifferential.D R (Polynomial R)) Polynomial.X

      The relative differential module of the univariate polynomial algebra R[X] is isomorphic to R[X] as an R[X]-module.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For