Neg

class proveit.numbers.Neg(A, *, styles=None)

Bases: proveit.numbers.NumberOperation

Methods Summary

as_int(self)	Convert a literal integer into a Python int.
deduce_in_number_set(self, number_set, …)	given a number set, attempt to prove that the given expression is in that number set using the appropriate closure theorem
distributed(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘distribution’.
distribution(self, \*\*defaults_config)	Distribute negation through a sum (Add) or over a fraction (Div), deducing and returning the equality between the original and distributed forms.
double_neg_simplification(self, …)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
double_neg_simplified(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘double_neg_simplification’.
factorization(self, the_factors[, pull, …])	Pull out the factor(s) from a negated expression, pulling it either to the “left” or “right”.
factorized(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘factorization’.
inner_neg_mult_simplification(self, idx, …)	Equivalence method to derive a simplification when negating a multiplication with a negated factor.
inner_neg_mult_simplified(expr, \*args, …)	Return an equivalent form of this expression derived via ‘inner_neg_mult_simplification’.
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
string(self, \*\*kwargs)	Return a string representation of the Expression.

Methods Documentation

as_int(self)

Convert a literal integer into a Python int. This only works if the operand is a literal int.

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

given a 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.

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

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

distribution(self, \*\*defaults_config)

Distribute negation through a sum (Add) or over a fraction (Div), deducing and returning the equality between the original and distributed forms.

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.

double_neg_simplification(self, \*\*defaults_config)

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

‘double_neg_simplified’ returns the right-hand side of ‘double_neg_simplification’. ‘double_neg_simplify’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘double_neg_simplification’ for the inner expression.

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

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

factorization(self, the_factors, pull='left', group_factors=None, group_remainder=None, \*\*defaults_config)

Pull out the factor(s) from a negated expression, pulling it either to the “left” or “right”. group_factors and group_remainder are not relevant here but kept for compatibility with other factor methods. Returns the equality that equates self to this new version. Give any assumptions necessary to prove that the operands are in the Complex numbers so that the associative and commutation theorems are applicable. FACTORING FROM NEGATION FROM A SUM NOT IMPLEMENTED YET.

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

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

Equivalence method to derive a simplification when negating a multiplication with a negated factor. For example, -(a*b*(-c)*d) = a*b*c*d. See Mult.neg_simplification where this may be used indirectly.

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

‘inner_neg_mult_simplified’ returns the right-hand side of ‘inner_neg_mult_simplification’. ‘inner_neg_mult_simplify’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘inner_neg_mult_simplification’ for the inner expression.

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

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

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

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