Exp

class proveit.numbers.Exp(base, exponent, *, styles=None)

Bases: proveit.numbers.NumberOperation

An Expression class to represent an exponentiation. Derive from Function since infix notation should not be a style option.

Methods Summary

deduce_in_number_set(self, number_set, …)	Attempt to prove that this exponentiation expression is in the given number set.
deduce_not_zero(self, \*\*defaults_config)	Prove that this exponential is not zero given that the base is not zero.
distributed(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘distribution’.
distribution(self, \*\*defaults_config)	Equate this exponential to a form in which the exponent is distributed over factors, or a power of a power reduces to a power of multiplied exponents. Examples: (a*b*c)^f = a^f * b^f * c^f (a/b)^f = (a^f / b^f).
expansion(self, \*\*defaults_config)	From self of the form x^n return x^n = x(x)…(x). For example, Exp(x, two).expansion(assumptions) should return: assumptions |- (x^2) = (x)(x). Currently only implemented explicitly for powers of n=2 and n=3.
formatted(self, format_type, \*\*kwargs)	Returns a formatted version of the expression for the given format_type (‘string’ or ‘latex’).
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
membership_object(self, element)
remake_arguments(self)	Yield the argument values or (name, value) pairs that could be used to recreate the Operation.
remake_constructor(self)	Method to call to reconstruct this Expression.
string(self, \*\*kwargs)	Return a string representation of the Expression.
style_options(self)	Returns the StyleOptions object for this Exp.
with_radical(self)
without_radical(self)

Methods Documentation

deduce_in_number_set(self, number_set, \*\*defaults_config)

Attempt to prove that this exponentiation expression is in the given number set.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_not_zero(self, \*\*defaults_config)

Prove that this exponential is not zero given that the base is not zero.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

distributed(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘distribution’.

distribution(self, \*\*defaults_config)

Equate this exponential to a form in which the exponent is distributed over factors, or a power of a power reduces to a power of multiplied exponents. Examples:

(a*b*c)^f = a^f * b^f * c^f (a/b)^f = (a^f / b^f)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘distributed’ returns the right-hand side of ‘distribution’. ‘distribute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘distribution’ for the inner expression.

expansion(self, \*\*defaults_config)

From self of the form x^n return x^n = x(x)…(x). For example, Exp(x, two).expansion(assumptions) should return: assumptions |- (x^2) = (x)(x). Currently only implemented explicitly for powers of n=2 and n=3.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘expanded’ returns the right-hand side of ‘expansion’. ‘expand’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘expansion’ for the inner expression.

formatted(self, format_type, \*\*kwargs)

Returns a formatted version of the expression for the given format_type (‘string’ or ‘latex’). In the keyword arguments, fence=True indicates that parenthesis around the sub-expression may be necessary to avoid ambiguity.

latex(self, \*\*kwargs)

Return a latex-formatted representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

membership_object(self, element)

remake_arguments(self)

Yield the argument values or (name, value) pairs that could be used to recreate the Operation.

remake_constructor(self)

Method to call to reconstruct this Expression. The default is the class name itself to use the __init__ method, but sometimes a different method is more appropriate for setting the proper style (e.g. the Frac method in proveit.numbers.division.divide which constructs a Div object with a different style). This constructor method must be in the same module as the class.

string(self, \*\*kwargs)

Return a string representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

style_options(self)

Returns the StyleOptions object for this Exp.

with_radical(self)

without_radical(self)