Common expressions for the theory of proveit.numbers.exponentiation

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

%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

prod_a_raise_ki__1_to_m = Mult(ExprRange(i, Exp(a, IndexedVar(k, i)), one, m))

prod_a_raise_ki__1_to_m:

Exp(a, n).get_styles()

prod_a_raise_bi__1_to_m = Mult(ExprRange(i, Exp(a, IndexedVar(b, i)), one, m))

prod_a_raise_bi__1_to_m:

prod_ai_raise_n__1_to_m = Mult(ExprRange(i, Exp(IndexedVar(a, i), n), one, m))

prod_ai_raise_n__1_to_m:

prod_ai_raise_b__1_to_m = Mult(ExprRange(i, Exp(IndexedVar(a, i), b), one, m))

prod_ai_raise_b__1_to_m:

nonzero_a_1_to_m = ExprTuple(ExprRange(i, NotEquals(IndexedVar(a, i), zero), one, m))

nonzero_a_1_to_m:

%end common

These common expressions may now be imported from the theory package: proveit.numbers.exponentiation