Hyperreal differentiation with an idempotent ultrafilter

Samuel Allen Alexander and Bryan Dawson

In light of the discussion on page 1 of differentiating numbers, we choose a way to define this and prove the Chain Rule.

def prim (n : ℤ) : ℤ

A "derivative".

Equations

• prim n = n - 1

def com (x : ℤ) (y : ℤ) : ℤ

A "composition".

Equations

• com x y = x * y

def starr (x : ℤ) (y : ℤ) : ℤ

A "multiplication".

Equations

• starr x y = x + y

theorem prim_com_eq_starr (x : ℤ) (y : ℤ) : prim (com x y) = starr (com (prim x) y) (prim y)

A "chain rule".