AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div

theorem AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div : ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : CharZero R] {p r : R} {z : ℤ}, z ≠ 0 → (z • r ∈ AddSubgroup.zmultiples p ↔ ∃ k, r - ↑k • (p / ↑z) ∈ AddSubgroup.zmultiples p)

In the context of a division ring `R` with characteristic zero, this theorem states that an integer `z` times a ring element `r` is a multiple of a ring element `p` if and only if `r` is `k/z` above a multiple of `p`, for some integer `k` where `0 ≤ k < |z|`. Here, `z` is not zero and `z • r` and `r - k • (p / z)` belonging to the subgroup of `R` generated by `p` essentially means they are multiples of `p`.

More concisely: In a division ring of characteristic zero, an integer `z` times a ring element `r` is a multiple of another ring element `p` if and only if `r` is a multiple of `p/z` plus a multiple of `p` with integer coefficient less than |z|.