gammaSet_eq_gcd_mul_divIntMap — Mathlib

English

For any r, v ∈ gammaSet(1,r,0) implies v = r • (divIntMap r v).

Русский

Для любого r, v ∈ gammaSet(1,r,0) выполнено v = r • (divIntMap r v).

LaTeX

$$$v = r \cdot (\mathrm{divIntMap}\ r\ v).$$$

Lean4

theorem gammaSet_eq_gcd_mul_divIntMap {r : ℕ} {v : Fin 2 → ℤ} (hv : v ∈ gammaSet 1 r 0) : v = r • (divIntMap r v) :=
  by
  by_cases hr : r = 0
  · have hv := hv.2
    simp only [hr, Fin.isValue, Int.gcd_eq_zero_iff, CharP.cast_eq_zero, zero_smul] at *
    ext i
    fin_cases i <;> simp [hv]
  · ext i
    simp_all [Pi.smul_apply, divIntMap, ← Int.mul_ediv_assoc _ (gammaSet_div_gcd hv i)]

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