vecMulSL_gcd — Mathlib

English

For any integer a and v with finGcdMap(v) = r, finGcdMap(a • v) = |a| · r.

Русский

Для целого a и вектора v с finGcdMap(v) = r выполняется finGcdMap(a • v) = |a| · r.

LaTeX

$$$\mathrm{finGcdMap}(a \cdot v) = |a| \cdot r.$$$

Lean4

/-- Right-multiplying a vector by a matrix in `SL(2, ℤ)` doesn't change its gcd. -/
theorem vecMulSL_gcd {v : Fin 2 → ℤ} (hab : finGcdMap v = r) (A : SL(2, ℤ)) : finGcdMap (v ᵥ* A.1) = r :=
  by
  have hvr : v = r • (v / r) := by
    ext i
    refine Eq.symm (Int.mul_ediv_cancel' ?_)
    fin_cases i <;> simp [← hab, Int.gcd_dvd_left, Int.gcd_dvd_right]
  rw [hvr, smul_vecMul]
  simpa using finGcdMap_smul r (Int.isCoprime_iff_gcd_eq_one.mp ((finGcdMap_div v hab).vecMulSL A))

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