isCoprime_of_dvd_isCoprime — Mathlib

English

If IsCoprime a.re a.im and b ∣ a, then IsCoprime b.re b.im.

Русский

Если a.re и a.im взаимно просты и b делит a, то b.re и b.im взаимно просты.

LaTeX

$$$IsCoprime(a_{\re}, a_{\im}) \land b \mid a \Rightarrow IsCoprime(b_{\re}, b_{\im})$$$

Lean4

theorem isCoprime_of_dvd_isCoprime {a b : ℤ√d} (hcoprime : IsCoprime a.re a.im) (hdvd : b ∣ a) : IsCoprime b.re b.im :=
  by
  apply isCoprime_of_dvd
  · rintro ⟨hre, him⟩
    obtain rfl : b = 0 := Zsqrtd.ext hre him
    rw [zero_dvd_iff] at hdvd
    simp [hdvd, im_zero, re_zero, not_isCoprime_zero_zero] at hcoprime
  · rintro z hz - hzdvdu hzdvdv
    apply hz
    obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
      rw [← intCast_dvd]
      apply dvd_trans _ hdvd
      rw [intCast_dvd]
      exact ⟨hzdvdu, hzdvdv⟩
    exact hcoprime.isUnit_of_dvd' ha hb

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