Divides

class proveit.numbers.Divides(x, y) represents the claim that x divides y (i.e. x|y)

Bases: proveit.numbers.divisibility.divides.DividesRelation

(equivalently, x is a factor of y, y is a multiple of x, or y/x is an integer). The axiomatic definition in Prove-It uses x|y = (y/x in Z), with no prerequisites on x and y. Extending DividesRelation allows us to have not only this weak relation class but also a strong relation class, DividesProper, the pair combined then allowing the calling of Divides.conclude_via_transitivity() utilizing the TransitiveRelation.conclude_via_transitivity() method.

Attributes Summary

known_left_sides
known_right_sides

Methods Summary

apply_transitivity(self, other, …)	From x|y (self) and y|z (other) derive and return x|z.
conclude(self, \*\*defaults_config)	Attempt to conclude the divisibility claim in various ways: (1) simple reflexivity (x|x); (2) simple x|0 for x ≠ 0; (3) simple x|xy or x|yx scenario (4) x^n | y^n if x|y is known or assumed (5) x|y if (x^n)|(y^n) is known or assumed (6) via transitivity.
conclude_via_factor(self, \*\*defaults_config)	Prove and return self of the form x|xy for x ≠ 0 and y in Ints
conclude_via_reflexivity(self, …)	Prove and return self of the form x|x with x ≠ 0.
conclude_via_zero_factor(self, …)	Prove and return self of the form x|0 for x ≠ 0
deduce_in_bool(self, \*\*defaults_config)	Deduce and return that this ‘Divides’ expression is in the Boolean set.
eliminate_common_exponent(self, …)	From self of the form (k^n)|(a^n), derive and return k|a.
eliminate_dividend_exponent(self, …)	From k|a^n (self), derive and return k|a if k is prime and a and n are integers.
introduce_common_exponent(self, exponent, …)	From self of the form (k)|(a), with integers k and a, derive and return k^n|a^n where n = exponent is a positive natural.

Attributes Documentation

known_left_sides = {}

known_right_sides = {}

Methods Documentation

apply_transitivity(self, other, \*\*defaults_config)

From x|y (self) and y|z (other) derive and return x|z. Will also check for y|z (self) and x|y (other) to return x|z.

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

conclude(self, \*\*defaults_config)

Attempt to conclude the divisibility claim in various ways: (1) simple reflexivity (x|x); (2) simple x|0 for x ≠ 0; (3) simple x|xy or x|yx scenario (4) x^n | y^n if x|y is known or assumed (5) x|y if (x^n)|(y^n) is known or assumed (6) via transitivity.

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

conclude_via_factor(self, \*\*defaults_config)

Prove and return self of the form x|xy for x ≠ 0 and y in Ints

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

conclude_via_reflexivity(self, \*\*defaults_config)

Prove and return self of the form x|x with x ≠ 0.

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

conclude_via_zero_factor(self, \*\*defaults_config)

Prove and return self of the form x|0 for x ≠ 0

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

deduce_in_bool(self, \*\*defaults_config)

Deduce and return that this ‘Divides’ expression is in the Boolean set.

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

eliminate_common_exponent(self, \*\*defaults_config)

From self of the form (k^n)|(a^n), derive and return k|a. k, a, must be integers, with n a positive integer. This method is called from the DividesRelation side_effects() method.

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

eliminate_dividend_exponent(self, \*\*defaults_config)

From k|a^n (self), derive and return k|a if k is prime and a and n are integers. Currently, this is only implement for k=2. This method is called from the DividesRelation.side_effects() method.

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

introduce_common_exponent(self, exponent, \*\*defaults_config)

From self of the form (k)|(a), with integers k and a, derive and return k^n|a^n where n = exponent is a positive natural.

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