P-derivation

In mathematics, more specifically differential algebra, a p"-derivation (for "p" a prime number) on a ring "R", is a mapping from "R" to "R" that satisfies certain conditions outlined directly below. The notion of a p"-derivation is related to that of a derivation in differential algebra. 
Definition.
Let "p" be a prime number. A "p"-derivation or Buium derivative on a ring formula_1 is a map formula_2 that satisfies the following "product rule":
and "sum rule":
as well as 
Note that in the "sum rule" we are not really dividing by "p", since all the relevant binomial coefficients in the numerator are divisible by "p", so this definition applies in the case when formula_1 has "p"-torsion.
Relation to Frobenius Endomorphisms.
A map formula_7 is a lift of the Frobenius endomorphism provided formula_8. An example of such a lift could come from the Artin map.
If formula_9 is a ring with a "p"-derivation, then the map formula_10 defines a ring endomorphism which is a lift of the Frobenius endomorphism. When the ring "R" is free the correspondence is a bijection.
Examples.
The quotient is well-defined because of Fermat's little theorem.
defines a "p"-derivation.