Generalizations of these are provided in a later file as
Note that the global
IsCoprime is not a straightforward generalization of
Nat.isCoprime_iff_coprime for the connection between the two.
Lemmas where one argument consists of addition of a multiple of the other
Lemmas where one argument consists of an addition of the other
Lemmas where one argument consists of a subtraction of the other
Represent a divisor of
m * n as a product of a divisor of
m and a divisor of
exists_dvd_and_dvd_of_dvd_mul for the more general but less constructive version for other
- One or more equations did not get rendered due to their size.