Description: The imaginary unit is the square root of negative 1. A lot of people like
to call this the "definition" of _i , but the definition of sqrtdf-sqrt has already been crafted with _i being mentioned explicitly,
and in any case it doesn't make too much sense to define a value based on
a function evaluated outside its domain. A more appropriate view is to
take ax-i2m1 or i2 as the "definition", and simply postulate the
existence of a number satisfying this property. This is the approach we
take here. (Contributed by Mario Carneiro, 10-Jul-2013)