gammaSet_div_gcd — Mathlib

English

For any r > 0, the map divIntMap r.cast provides a bijection between gammaSet(1,r,0) and gammaSet(1,1,0).

Русский

Для r > 0 отображение divIntMap r.cast образует биекцию между gammaSet(1,r,0) и gammaSet(1,1,0).

LaTeX

$$$\text{BijOn} \, (\mathrm{divIntMap}\ r.{\mathrm{cast}}) \, (\gammaSet(1,r,0)) \ (\gammaSet(1,1,0)).$$$

Lean4

theorem gammaSet_div_gcd {r : ℕ} {v : Fin 2 → ℤ} (hv : v ∈ (gammaSet 1 r 0)) (i : Fin 2) : (r : ℤ) ∣ v i := by
  fin_cases i <;> simp [← hv.2, Int.gcd_dvd_left, Int.gcd_dvd_right]

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