Theorems · Definition · commutative algebra

Polynomial.mkDerivationEquiv

(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

Polynomial.mkDerivation as a linear equivalence.

Defined in

Mathlib.Algebra.Polynomial.Derivation

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleModuleIsScalarTower