# Documentation

Mathlib.Algebra.Ring.Divisibility.Lemmas

# 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] [] [] {x : R} {y : R} (m : M) (h : x y) :
x m y
theorem dvd_nsmul_of_dvd {R : Type u_1} {x : R} {y : R} (n : ) (h : x y) :
x n y
theorem dvd_zsmul_of_dvd {R : Type u_1} [] {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) [] (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) [] (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