English
Let z ∈ ℤ and a ∈ ℤ√d. Then z divides a in ℤ√d if and only if z divides a.re and z divides a.im.
Русский
Пусть z ∈ ℤ и a ∈ ℤ√d. Тогда z делит a в ℤ√d тогда, когда z делит a.re и z делит a.im.
LaTeX
$$$ (z : \mathbb{Z}) \mid a \text{ in } \mathbb{Z}[\sqrt{d}] \iff z \mid a_{\re} \land z \mid a_{\im}$$$
Lean4
theorem intCast_dvd (z : ℤ) (a : ℤ√d) : ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im :=
by
constructor
· rintro ⟨x, rfl⟩
simp only [add_zero, re_intCast, zero_mul, im_mul, dvd_mul_right, and_self_iff, re_mul, mul_zero, im_intCast]
· rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩
use ⟨r, i⟩
rw [smul_val, Zsqrtd.ext_iff]
exact ⟨hr, hi⟩