(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