Axioms for the theory of proveit.numbers.number_sets.complex_numbers

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

%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.

imaginary_number_def = Equals(Mult(i, i), Neg(one))

imaginary_number_def:

complex_numbers_def = Forall((a, b), InSet(Add(a, Mult(i, b)), Complex), domain=Real)

complex_numbers_def:

conjugate_def = Forall((a, b), Equals(Conjugate(Add(a, Mult(i, b))),
                                      subtract(a, Mult(i, b))))

conjugate_def:

%end axioms

These axioms may now be imported from the theory package: proveit.numbers.number_sets.complex_numbers