intCast_dvd — Mathlib

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⟩

Похожие утверждения