Mult

class proveit.numbers.Mult(*operands, styles=None)

Bases: proveit.numbers.NumberOperation

Attributes Summary

Methods Summary

associated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘association’.
association(self, start_idx, length, …)	Given numerical operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, (a * b * … * y * z) = (a * b … * (l * … * m) * … * y * z).
cancelation(self, term_to_cancel, …)	Deduce and return an equality between self and a form in which the given factor has been canceled in a numerator (or factor) and denominator.
cancelations(self, \*\*defaults_config)	Deduce and return an equality between self and a form in which all simple division cancelations are performed across the factors of this multiplication.
combined_exponents(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘combining_exponents’.
commutation(self[, init_idx, final_idx])	Given numerical operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx.
commuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘commutation’.
conversion_to_addition(self, \*\*defaults_config)	From multiplication by an integer as the first factor, derive and return the equivalence of this multiplication to a repeated addition; for example, 3*c = c + c + c.
deduce_divided_by(self, divisor, …)	Deduce that the product represented by Mult(a,b) is divisible by the divisor a or b. For example, Mult(a, b).deduce_divided_by(a) returns |- Divides(a, Mult(a,b)), that is |- a|ab, (assuming complex a≠0 and integer b). Later: possibly consider an Equals(divisor,self.lhs) case?.
deduce_in_number_set(self, number_set, …)	Attempt to prove that this product is in the given number_set.
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 direct factors as well as grouped factors and in fraction factors.
disassociated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘disassociation’.
disassociation(self, idx, \*\*defaults_config)	Given numerical operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example, (a * b … * (l * … * m) * … * y* z) = (a * b * … * y * z) Multiple indices can be provided for multiple disassociations simultaneously, e.g. expr.disassociation(2, 3, 4).
distributed(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘distribution’.
distribution(self[, idx, left_factors, …])	Distribute through the operand at the given index. Returns the equality that equates self to this new version. Examples: a (b + c + a) d = a b d + a c d + a a d a (b - c) d = a b d - a c d a (sum_x f(x)) c = sum_x a f(x) c (a/b)*(c/d) = (a*b)/(c*d) Example for a distribute_all_sums: recursively looks for first add or sum to distribute through (a+b)(c+d)ef = a(c+d)ef + b(c+d)ef = acef + adef + bcef + bdef.
factorization(self, the_factors_or_index[, …])	Return the proven factorization (equality with the factored form) from pulling the factor(s) from this product to the “left” or “right”.
factorized(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘factorization’.
group_commutation(self, init_idx, final_idx, …)	Given numerical operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx.
group_commuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘group_commutation’.
index(self, the_factor[, also_return_num])	Return the starting index of the_factor, which may be a single operand, a list of consecutive operands, or a Mult expression that represents the product of the list of consecutive operands.
neg_simplification(self, idx, …)	Equivalence method that derives a simplification in which a specific negated factor, at the given index, is factored out. For example: w*(-x)*y*z = -(w*x*y*z).
neg_simplifications(self, \*\*defaults_config)	Equivalence method that derives a simplification in which negated factors are factored out. For example: (-w)*(-x)*y*(-z) = -(w*x*y*z).
one_elimination(self, idx, \*\*defaults_config)	Equivalence method that derives a simplification in which a single factor of one, at the given index, is eliminated. For example: x*y*1*z = x*y*z.
one_eliminations(self, \*\*defaults_config)	Equivalence method that derives a simplification in which factors of one are eliminated. For example: x*1*y*1*z*1 = x*y*z.

Attributes Documentation

Methods Documentation

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

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

association(self, start_idx, length, \*\*defaults_config)

Given numerical operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, (a * b * … * y * z) =

(a * b … * (l * … * m) * … * y * z)

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

‘associated’ returns the right-hand side of ‘association’. ‘associate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘association’ for the inner expression.

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

Deduce and return an equality between self and a form in which the given factor has been canceled in a numerator (or factor) and denominator. For example, [a*b*c*(1/b)].cancelation(b) would return a*b*c*(1/b) = a*c

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 across the factors of this multiplication.

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 ‘combining_exponents’.

commutation(self, init_idx=None, final_idx=None, \*\*defaults_config)

Given numerical operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx. For example, (a · b · … · y · z) = (a · … · y · b · z) via init_idx = 1 and final_idx = -2.

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

‘commuted’ returns the right-hand side of ‘commutation’. ‘commute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘commutation’ for the inner expression.

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

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

conversion_to_addition(self, \*\*defaults_config)

From multiplication by an integer as the first factor, derive and return the equivalence of this multiplication to a repeated addition; for example, 3*c = c + c + c.

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

‘converted_to_addition’ returns the right-hand side of ‘conversion_to_addition’. ‘convert_to_addition’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘conversion_to_addition’ for the inner expression.

deduce_divided_by(self, divisor, \*\*defaults_config)

Deduce that the product represented by Mult(a,b) is divisible by the divisor a or b. For example,

Mult(a, b).deduce_divided_by(a)

returns |- Divides(a, Mult(a,b)), that is |- a|ab, (assuming complex a≠0 and integer b). Later: possibly consider an Equals(divisor,self.lhs) case?

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

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

Attempt to prove that this product is in the given number_set.

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 direct factors as well as grouped factors and in fraction factors.

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.

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

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

disassociation(self, idx, \*\*defaults_config)

Given numerical operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example, (a * b … * (l * … * m) * … * y* z)

= (a * b * … * y * z)

Multiple indices can be provided for multiple disassociations simultaneously, e.g. expr.disassociation(2, 3, 4)

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

‘disassociated’ returns the right-hand side of ‘disassociation’. ‘disassociate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘disassociation’ for the inner expression.

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

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

distribution(self, idx=None, \*, left_factors=None, right_factors=None, \*\*defaults_config)

Distribute through the operand at the given index. Returns the equality that equates self to this new version. Examples:

a (b + c + a) d = a b d + a c d + a a d a (b - c) d = a b d - a c d a (sum_x f(x)) c = sum_x a f(x) c (a/b)*(c/d) = (a*b)/(c*d)

Example for a distribute_all_sums:

recursively looks for first add or sum to distribute through (a+b)(c+d)ef = a(c+d)ef + b(c+d)ef

= acef + adef + bcef + bdef

For more flexibility, ‘left_factors’ and ‘right_factors’ may be specified to indicate subsets of the factors to distribute on the left vs right. The ‘left_factors’ and ‘right_factors’ may be provided as indices instead. Examples:

a b (c + d) e f = a (b c f + b d f) e

with left_factors: [b], right_factors: [f] or left_factors: [1], right_factors: [4]

a b (c + d) e f = a (f c b e + f d b e)

with left_factors: [f], right_factors: [b, e] or left_factors: [4], right_factors: [1, 3] If one of these is specified but not the other, the emtpy set is used for the one that isn’t specified.

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.

factorization(self, the_factors_or_index, pull='left', group_factors=True, group_remainder=False, \*\*defaults_config)

Return the proven factorization (equality with the factored form) from pulling the factor(s) from this product to the “left” or “right”. the_factors_or_index may be an iterable or a Mult; in either case, the individual factors will be pulled together in the pull direction. If there are multiple occurrences, the first occurrence is used. If group_factors is True, the factors are grouped together as a sub-product. If group_remainder is True and there are multiple remaining operands, then these remaining

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

‘factorized’ returns the right-hand side of ‘factorization’. ‘factor’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘factorization’ for the inner expression.

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

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

group_commutation(self, init_idx, final_idx, length, disassociate=True, \*\*defaults_config)

Given numerical operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx. final_idx+length). It will do this by performing association first. If disassocate is True, it will be disassociated afterwards.

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

‘group_commuted’ returns the right-hand side of ‘group_commutation’. ‘group_commute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘group_commutation’ for the inner expression.

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

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

index(self, the_factor, also_return_num=False)

Return the starting index of the_factor, which may be a single operand, a list of consecutive operands, or a Mult expression that represents the product of the list of consecutive operands. If also_return_num is True, return a tuple of the index and number of operands for the_factor.

neg_simplification(self, idx, \*\*defaults_config)

Equivalence method that derives a simplification in which a specific negated factor, at the given index, is factored out. For example:

w*(-x)*y*z = -(w*x*y*z)

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

‘simplified_negation’ returns the right-hand side of ‘neg_simplification’. ‘simplify_negation’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘neg_simplification’ for the inner expression.

neg_simplifications(self, \*\*defaults_config)

Equivalence method that derives a simplification in which negated factors are factored out. For example:

(-w)*(-x)*y*(-z) = -(w*x*y*z)

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

‘simplified_negations’ returns the right-hand side of ‘neg_simplifications’. ‘simplify_negations’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘neg_simplifications’ for the inner expression.

one_elimination(self, idx, \*\*defaults_config)

Equivalence method that derives a simplification in which a single factor of one, at the given index, is eliminated. For example:

x*y*1*z = x*y*z

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

‘eliminated_one’ returns the right-hand side of ‘one_elimination’. ‘eliminate_one’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘one_elimination’ for the inner expression.

one_eliminations(self, \*\*defaults_config)

Equivalence method that derives a simplification in which factors of one are eliminated. For example:

x*1*y*1*z*1 = x*y*z

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

‘eliminated_ones’ returns the right-hand side of ‘one_eliminations’. ‘eliminate_ones’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘one_eliminations’ for the inner expression.