Lemmas about divisibility in rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
has_dvd.dvd.linear_comb
{α : Type u_1}
[non_unital_comm_semiring α]
{d x y : α}
(hdx : d ∣ x)
(hdy : d ∣ y)
(a b : α) :
theorem
dvd_of_dvd_neg
{α : Type u_1}
[semigroup α]
[has_distrib_neg α]
{a b : α}
(h : a ∣ -b) :
a ∣ b
theorem
dvd_of_neg_dvd
{α : Type u_1}
[semigroup α]
[has_distrib_neg α]
{a b : α}
(h : -a ∣ b) :
a ∣ b
If an element a divides another element c in a commutative ring, a divides the sum of another element b with c iff a divides b.
If an element a divides another element b in a commutative ring, a divides the sum of b and another element c iff a divides c.