Hypercomplex numbers
/-- x + iy where x and y are Hyperreals -/
structure hypercomplex :
(x : hypereal)
(y : hyperreal)
“Hyperreals extend reals: there exist infinitesimal and infinite elements respectively smaller and bigger than any positive real number.”