Div

class proveit.numbers.Div(numerator, denominator, *, styles=None)

Bases: proveit.numbers.NumberOperation

Methods Summary

cancelation(self, term_to_cancel, …)	Deduce and return an equality between self and a form in which the given operand has been canceled on the numerator and denominator.
cancelations(self, \*\*defaults_config)	Deduce and return an equality between self and a form in which all simple division cancelations are performed.
combined_exponents(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘exponent_combination’.
deduce_in_number_set(self, number_set, …)	Given a number set number_set, attempt to prove that the given expression is in that number set using the appropriate closure theorem.
deep_eliminated_ones(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘deep_one_eliminations’.
deep_one_eliminations(self, \*\*defaults_config)	Eliminate ones from the numerator, the denominator, and as a division by one.
distribution(self, \*\*defaults_config)	Distribute the denominator through the numerator, returning the equality that equates self to this new version. Examples: \((a + b + c) / d = a / d + b / d + c / d\) \((a - b) / d = a / d - b / d\) \(\left(\sum_x f(x)\right / y = \sum_x [f(x) / y]\) Give any assumptions necessary to prove that the operands are in the Complex numbers so that the associative and commutation theorems are applicable.
exponent_combination(self[, start_idx, end_idx])	Equates $a^m/a^n$ to $a^{m-n} or $a^c/b^c$ to $(a/b)^c$.
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
remake_constructor(self)	Method to call to reconstruct this Expression.
style_options(self)	Return the StyleOptions object for this Div.
with_fraction_style(self)
with_inline_style(self)

Methods Documentation

cancelation(self, term_to_cancel, \*\*defaults_config)

Deduce and return an equality between self and a form in which the given operand has been canceled on the numerator and denominator. For example, [(a*b)/(b*c)].cancelation(b) would return (a*b)/(b*c) = a / c. Assumptions or previous work might be required to establish that the term_to_cancel is non-zero.

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

‘canceled’ returns the right-hand side of ‘cancelation’. ‘cancel’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘cancelation’ for the inner expression.

cancelations(self, \*\*defaults_config)

Deduce and return an equality between self and a form in which all simple division cancelations are performed.

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

‘all_canceled’ returns the right-hand side of ‘cancelations’. ‘all_cancel’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘cancelations’ for the inner expression.

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

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

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

Given a number set number_set, attempt to prove that the given expression is in that number set using the appropriate closure theorem.

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

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

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

deep_one_eliminations(self, \*\*defaults_config)

Eliminate ones from the numerator, the denominator, and as a division by one.

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

‘deep_eliminated_ones’ returns the right-hand side of ‘deep_one_eliminations’. ‘deep_eliminate_ones’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘deep_one_eliminations’ for the inner expression.

distribution(self, \*\*defaults_config)

Distribute the denominator through the numerator, returning the equality that equates self to this new version. Examples:

\((a + b + c) / d = a / d + b / d + c / d\) \((a - b) / d = a / d - b / d\) \(\left(\sum_x f(x)\right / y = \sum_x [f(x) / y]\)

Give any assumptions necessary to prove that the operands are in the Complex numbers so that the associative and commutation theorems are applicable.

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.

exponent_combination(self, start_idx=None, end_idx=None, \*\*defaults_config)

Equates $a^m/a^n$ to $a^{m-n} or $a^c/b^c$ to $(a/b)^c$.

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

‘combined_exponents’ returns the right-hand side of ‘exponent_combination’. ‘combine_exponents’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘exponent_combination’ for the inner expression.

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

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.

style_options(self)

Return the StyleOptions object for this Div.

with_fraction_style(self)

with_inline_style(self)