intCast_dvd_intCast — Mathlib

English

For all integers a,b, the integer a, viewed as an element of ℤ√d, divides b in ℤ√d if and only if a divides b in ℤ.

Русский

Для всех целых a, b: целое a, как элемент ℤ√d, делит b в ℤ√d тогда, когда a делит b в ℤ.

LaTeX

$$$(a : \mathbb{Z}\sqrt{d}) \mid b \iff a \mid b$$$

Lean4

@[simp, norm_cast]
theorem intCast_dvd_intCast (a b : ℤ) : (a : ℤ√d) ∣ b ↔ a ∣ b :=
  by
  rw [intCast_dvd]
  constructor
  · rintro ⟨hre, -⟩
    rwa [re_intCast] at hre
  · rw [re_intCast, im_intCast]
    exact fun hc => ⟨hc, dvd_zero a⟩

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