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 : R} {y : R} (m : M) (h : x ∣ y) : x ∣ m • y

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

theorem dvd_zsmul_of_dvd {R : Type u_1} [NonUnitalRing R] {x : R} {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 : R} {y : R} {n : ℕ} {m : ℕ} {p : ℕ} (hp : n + m ≤ p + 1) [Semiring R] (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 : R} {y : R} {n : ℕ} {m : ℕ} {p : ℕ} (hp : n + m ≤ p + 1) [Semiring R] (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 : R} {y : R} {n : ℕ} {m : ℕ} {p : ℕ} (hp : n + m ≤ p + 1) [Ring R] (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 : R} {y : R} {n : ℕ} {m : ℕ} {p : ℕ} (hp : n + m ≤ p + 1) [Ring R] (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 : R} {y : R} {n : ℕ} {m : ℕ} {p : ℕ} (hp : n + m ≤ p + 1) [Ring R] (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 : R} {y : R} {n : ℕ} {m : ℕ} {p : ℕ} (hp : n + m ≤ p + 1) [Ring R] (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 : R} {y : R} {n : ℕ} {m : ℕ} {p : ℕ} (hp : n + m ≤ p + 1) [Ring R] (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 : R} {y : R} {n : ℕ} {m : ℕ} {p : ℕ} (hp : n + m ≤ p + 1) [Ring R] (h_comm : Commute x y) (hy : y ^ n = 0) : (x + y) ^ m ∣ x ^ p