Lemmas about divisibility in rings

Main results:

• dvd_smul_of_dvd: stating that x ∣ y → x ∣ m • y for any scalar m.
• Commute.pow_dvd_add_pow_of_pow_eq_zero_right: stating that if y is nilpotent then x ^ m ∣ (x + y) ^ p for sufficiently large p (together with many variations for convenience).

theorem dvd_smul_of_dvd {R : Type u_1} {M : Type u_2} [SMul M R] [Semigroup R] [SMulCommClass M R R] {x y : R} (m : M) (h : x ∣ y) : x ∣ m • y

theorem dvd_nsmul_of_dvd {R : Type u_1} [NonUnitalSemiring R] {x y : R} (n : ℕ) (h : x ∣ y) : x ∣ n • y

theorem dvd_zsmul_of_dvd {R : Type u_1} [NonUnitalRing R] {x y : R} (z : ℤ) (h : x ∣ y) : x ∣ z • y

theorem Commute.pow_dvd_add_pow_of_pow_eq_zero_right {R : Type u_1} {x y : R} {n m p : ℕ} [Semiring R] (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hy : y ^ n = 0) : x ^ m ∣ (x + y) ^ p

theorem Commute.pow_dvd_add_pow_of_pow_eq_zero_left {R : Type u_1} {x y : R} {n m p : ℕ} [Semiring R] (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hx : x ^ n = 0) : y ^ m ∣ (x + y) ^ p

theorem Commute.pow_dvd_pow_of_sub_pow_eq_zero {R : Type u_1} {x y : R} {n m p : ℕ} [Ring R] (hp : n + m ≤ p + 1) (h_comm : Commute x y) (h : (x - y) ^ n = 0) : x ^ m ∣ y ^ p

theorem Commute.pow_dvd_pow_of_add_pow_eq_zero {R : Type u_1} {x y : R} {n m p : ℕ} [Ring R] (hp : n + m ≤ p + 1) (h_comm : Commute x y) (h : (x + y) ^ n = 0) : x ^ m ∣ y ^ p

theorem Commute.pow_dvd_sub_pow_of_pow_eq_zero_right {R : Type u_1} {x y : R} {n m p : ℕ} [Ring R] (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hy : y ^ n = 0) : x ^ m ∣ (x - y) ^ p

theorem Commute.pow_dvd_sub_pow_of_pow_eq_zero_left {R : Type u_1} {x y : R} {n m p : ℕ} [Ring R] (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hx : x ^ n = 0) : y ^ m ∣ (x - y) ^ p

theorem Commute.add_pow_dvd_pow_of_pow_eq_zero_right {R : Type u_1} {x y : R} {n m p : ℕ} [Ring R] (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hx : x ^ n = 0) : (x + y) ^ m ∣ y ^ p

theorem Commute.add_pow_dvd_pow_of_pow_eq_zero_left {R : Type u_1} {x y : R} {n m p : ℕ} [Ring R] (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hy : y ^ n = 0) : (x + y) ^ m ∣ x ^ p

theorem dvd_mul_sub_mul_mul_left_of_dvd {R : Type u_1} [CommRing R] {p a b c d x y : R} (h1 : p ∣ a * x + b * y) (h2 : p ∣ c * x + d * y) : p ∣ (a * d - b * c) * x

theorem dvd_mul_sub_mul_mul_right_of_dvd {R : Type u_1} [CommRing R] {p a b c d x y : R} (h1 : p ∣ a * x + b * y) (h2 : p ∣ c * x + d * y) : p ∣ (a * d - b * c) * y

theorem dvd_mul_sub_mul_mul_gcd_of_dvd {R : Type u_1} [CommRing R] {p a b c d x y : R} [GCDMonoid R] (h1 : p ∣ a * x + b * y) (h2 : p ∣ c * x + d * y) : p ∣ (a * d - b * c) * gcd x y

@[simp]

theorem associated_abs_left_iff {R : Type u_1} [Ring R] [LinearOrder R] {x y : R} : Associated |x| y ↔ Associated x y

@[simp]

theorem associated_abs_right_iff {R : Type u_1} [Ring R] [LinearOrder R] {x y : R} : Associated x |y| ↔ Associated x y

theorem Associated.abs_left {R : Type u_1} [Ring R] [LinearOrder R] {x y : R} : Associated x y → Associated |x| y

Alias of the reverse direction of associated_abs_left_iff.

theorem Associated.abs_right {R : Type u_1} [Ring R] [LinearOrder R] {x y : R} : Associated x y → Associated x |y|

Alias of the reverse direction of associated_abs_right_iff.