finGcdMap_div — Mathlib

English

If r > 0 and v ∈ Fin 2 → ℤ with finGcdMap(v) = r, then finGcdMap(v/r) = 1; i.e. the divided vector is coprime.

Русский

Пусть r>0 и v ∈ ℤ^2 с gcd(v_0,v_1)=r. Тогда gcd(v_0/r,v_1/r)=1.

LaTeX

$$$\text{If } r>0\text{ and } \mathrm{finGcdMap}(v)=r,\ \mathrm{IsCoprime}\left(\frac{v_0}{r},\frac{v_1}{r}\right).$$$

Lean4

theorem finGcdMap_div {r : ℕ} [NeZero r] (v : Fin 2 → ℤ) (hv : finGcdMap v = r) : IsCoprime ((v / r) 0) ((v / r) 1) :=
  by
  rw [← hv]
  apply isCoprime_div_gcd_div_gcd_of_gcd_ne_zero
  have := NeZero.ne r
  aesop

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