Lemmas about divisibility in rings #
Main results: #
dvd_smul_of_dvd
: stating thatx ∣ y → x ∣ m • y
for any scalarm
.Commute.pow_dvd_add_pow_of_pow_eq_zero_right
: stating that ify
is nilpotent thenx ^ m ∣ (x + y) ^ p
for sufficiently largep
(together with many variations for convenience).