In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import a, b
from proveit.logic import Forall, Equals, InSet
from proveit.numbers import one, i, Real, Complex, Add, subtract, Neg, Mult, Conjugate
In [2]:
%begin axioms
Defining axioms for theory 'proveit.numbers.number_sets.complex_numbers'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

The imaginary number is defined as a number that squares to -1.

In [3]:
imaginary_number_def = Equals(Mult(i, i), Neg(one))
In [4]:
complex_numbers_def = Forall((a, b), InSet(Add(a, Mult(i, b)), Complex), domain=Real)
In [5]:
conjugate_def = Forall((a, b), Equals(Conjugate(Add(a, Mult(i, b))),
                                      subtract(a, Mult(i, b))))
In [6]:
%end axioms
These axioms may now be imported from the theory package: proveit.numbers.number_sets.complex_numbers