Theorems · Definition · commutative algebra

Polynomial.mkDerivation

(R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          [inst_3 : Module (Polynomial R) A] →
            [inst_4 : IsScalarTower R (Polynomial R) A] → A →ₗ[R] Derivation R (Polynomial R) A

The derivation on R[X] that takes the value a on X.

Defined in

Mathlib.Algebra.Polynomial.Derivation

Cited by

5 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleModuleIsScalarTower