Lemmas about quotients in characteristic zero

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

z • r is a multiple of p iff r is pk/z above a multiple of p, where 0 ≤ k < |z|.

theorem AddSubgroup.nsmul_mem_zmultiples_iff_exists_sub_div {R : Type u_1} [DivisionRing R] [CharZero R] {p : R} {r : R} {n : ℕ} (hn : n ≠ 0) : n • r ∈ AddSubgroup.zmultiples p ↔ ∃ (k : Fin n), r - ↑k • (p / ↑n) ∈ AddSubgroup.zmultiples p

theorem QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff {R : Type u_1} [DivisionRing R] [CharZero R] {p : R} {ψ : R ⧸ AddSubgroup.zmultiples p} {θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) : z • ψ = z • θ ↔ ∃ (k : Fin (Int.natAbs z)), ψ = θ + ↑(↑k • (p / ↑z))

theorem QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff {R : Type u_1} [DivisionRing R] [CharZero R] {p : R} {ψ : R ⧸ AddSubgroup.zmultiples p} {θ : R ⧸ AddSubgroup.zmultiples p} {n : ℕ} (hz : n ≠ 0) : n • ψ = n • θ ↔ ∃ (k : Fin n), ψ = θ + ↑k • ↑(p / ↑n)