Common expressions for the theory of proveit.numbers.exponentiation

In [1]:
import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit import ExprTuple, ExprRange, IndexedVar
from proveit.logic import NotEquals
from proveit import a, b, i, k, m, n
from proveit.numbers import Mult, Exp, one, zero
In [2]:
%begin common
Defining common sub-expressions for theory 'proveit.numbers.exponentiation'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions
In [3]:
prod_a_raise_ki__1_to_m = Mult(ExprRange(i, Exp(a, IndexedVar(k, i)), one, m))
In [4]:
Exp(a, n).get_styles()
In [5]:
prod_a_raise_bi__1_to_m = Mult(ExprRange(i, Exp(a, IndexedVar(b, i)), one, m))
In [6]:
prod_ai_raise_n__1_to_m = Mult(ExprRange(i, Exp(IndexedVar(a, i), n), one, m))
In [7]:
prod_ai_raise_b__1_to_m = Mult(ExprRange(i, Exp(IndexedVar(a, i), b), one, m))
In [8]:
nonzero_a_1_to_m = ExprTuple(ExprRange(i, NotEquals(IndexedVar(a, i), zero), one, m))
In [9]:
%end common
These common expressions may now be imported from the theory package: proveit.numbers.exponentiation