Documentation

Mathlib.Algebra.Ring.Divisibility.Lemmas

Lemmas about divisibility in rings #

Main results: #

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 : } [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 : R} {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 : R} {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 : R} {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 : R} {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 : R} {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 : R} {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 : R} {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 : R} {a : R} {b : R} {c : R} {d : R} {x : R} {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 : R} {a : R} {b : R} {c : R} {d : R} {x : R} {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 : R} {a : R} {b : R} {c : R} {d : R} {x : R} {y : R} [IsDomain R] [GCDMonoid R] (h1 : p a * x + b * y) (h2 : p c * x + d * y) :
p (a * d - b * c) * gcd x y