English
In a Division Ring of characteristic zero, z ≠ 0 implies that z · r is a zmultiples of p iff there exists k with 0 ≤ k < |z| such that r − k(p/z) lies in zmultiples(p).
Русский
В дивизионном кольце характеристика ноль; для z ≠ 0 верно: z·r ∈ zmultiples(p) эквивалентно существованию k; 0 ≤ k < |z| такие, что r − k(p/z) ∈ zmultiples(p).
LaTeX
$$$ z \neq 0 \Rightarrow z\cdot r \in \operatorname{zmultiples}(p) \iff \exists k: Fin(z^{-1}) ,\ r - (k) (p/z) \in \operatorname{zmultiples}(p) $$$
Lean4
/-- `z • r` is a multiple of `p` iff `r` is `k * (p / z)` above a multiple of `p`, where
`0 ≤ k < |z|`. -/
theorem zsmul_mem_zmultiples_iff_exists_sub_div {r : R} {z : ℤ} (hz : z ≠ 0) :
z • r ∈ AddSubgroup.zmultiples p ↔ ∃ k : Fin z.natAbs, r - (k : ℕ) • (p / z : R) ∈ AddSubgroup.zmultiples p :=
by
rw [AddSubgroup.mem_zmultiples_iff]
simp_rw [AddSubgroup.mem_zmultiples_iff, div_eq_mul_inv, ← smul_mul_assoc, eq_sub_iff_add_eq]
have hz' : (z : R) ≠ 0 := Int.cast_ne_zero.mpr hz
conv_rhs => simp +singlePass only [← (mul_right_injective₀ hz').eq_iff]
simp_rw [← zsmul_eq_mul, smul_add, ← mul_smul_comm, zsmul_eq_mul (z : R)⁻¹, mul_inv_cancel₀ hz', mul_one, ←
natCast_zsmul, smul_smul, ← add_smul]
constructor
· rintro ⟨k, h⟩
simp_rw [← h]
refine ⟨⟨(k % z).toNat, ?_⟩, k / z, ?_⟩
· rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
exact (Int.emod_lt_abs _ hz).trans_eq (Int.abs_eq_natAbs _)
rw [Fin.val_mk, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
nth_rewrite 3 [← Int.mul_ediv_add_emod k z]
rfl
· rintro ⟨k, n, h⟩
exact ⟨_, h⟩
