vecMul_SL2_mem_gammaSet — Mathlib

English

An abbreviation of the map which divides a integer vector by an integer.

Русский

Сокращение отображения, делящего целочисленный вектор на целое число.

LaTeX

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

Lean4

/-- Right-multiplying by `γ ∈ SL(2, ℤ)` sends `gammaSet N a` to `gammaSet N (a ᵥ* γ)`. -/
theorem vecMul_SL2_mem_gammaSet {v : Fin 2 → ℤ} (hv : v ∈ gammaSet N r a) (γ : SL(2, ℤ)) :
    v ᵥ* γ ∈ gammaSet N r (a ᵥ* γ) := by
  refine ⟨?_, vecMulSL_gcd hv.2 γ⟩
  have := RingHom.map_vecMul (m := Fin 2) (n := Fin 2) (Int.castRingHom (ZMod N)) γ v
  simp only [eq_intCast, Int.coe_castRingHom] at this
  simp_rw [Function.comp_def, this, hv.1]
  simp

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