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).
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)
:
@[simp]
@[simp]
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
.