Axioms for the theory of proveit.numbers.multiplication

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 ExprRange
from proveit.logic import Forall, Equals, Set
from proveit import a, b, k, n, x
from proveit.core_expr_types import a_1_to_n
from proveit.numbers import one, two, Mult, Add, Complex, Natural, Exp

%begin axioms

Defining axioms for theory 'proveit.numbers.multiplication'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

mult_def = \
    Forall((n, x), Equals(Mult(n, x), Add(ExprRange(k, x, one, n))),
           domains=(Natural, Complex))

mult_def:

empty_mult = Equals(Mult(), one)

empty_mult:

multi_mult_def = \
    Forall(n, Forall((a_1_to_n, b), 
                     Equals(Mult(a_1_to_n, b), Mult(Mult(a_1_to_n), b)),
                     domain=Complex),
           domain=Natural)

multi_mult_def:

%end axioms

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