English
For v ∈ Fin 2 → ℤ, v ∈ gammaSet 1 1 0 iff IsCoprime(v_0,v_1).
Русский
Пусть v ∈ ℤ^2; тогда v ∈ gammaSet(1,1,0) тогда и только тогда, когда gcd(v_0,v_1)=1.
LaTeX
$$$v \in \gammaSet(1,1,0) \iff \mathrm{IsCoprime}(v_0,v_1).$$$
Lean4
/-- The bijection between `GammaSets` given by multiplying by an element of `SL(2, ℤ)`. -/
def gammaSetEquiv (γ : SL(2, ℤ)) : gammaSet N r a ≃ gammaSet N r (a ᵥ* γ)
where
toFun v := ⟨v.1 ᵥ* γ, vecMul_SL2_mem_gammaSet v.2 γ⟩
invFun
v :=
⟨v.1 ᵥ* ↑(γ⁻¹), by
have := vecMul_SL2_mem_gammaSet v.2 γ⁻¹
rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul] at this
simpa only [SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom, map_inv,
mul_inv_cancel, SpecialLinearGroup.coe_one, vecMul_one]⟩
left_inv
v := by
simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_cancel, SpecialLinearGroup.coe_one, vecMul_one]
right_inv
v := by
simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_cancel, SpecialLinearGroup.coe_one, vecMul_one]
