ModularGroup_T_pow_mem_Gamma — Mathlib

English

For integers N, M with N dividing M, the matrix T^M lies in Gamma(|N|).

Русский

Для целых N, M с N|M, матрица T^M принадлежит Gamma(|N|).

LaTeX

$$(ModularGroup.T)^M ∈ Gamma(|N|)$$

Lean4

theorem ModularGroup_T_pow_mem_Gamma (N M : ℤ) (hNM : N ∣ M) : (ModularGroup.T ^ M) ∈ Gamma (Int.natAbs N) :=
  by
  simp only [Gamma_mem, Fin.isValue, ModularGroup.coe_T_zpow, of_apply, cons_val', cons_val_zero, empty_val',
    cons_val_fin_one, Int.cast_one, cons_val_one, Int.cast_zero, and_self, and_true, true_and]
  refine Iff.mpr (ZMod.intCast_zmod_eq_zero_iff_dvd M (Int.natAbs N)) ?_
  simp only [Int.natCast_natAbs, abs_dvd, hNM]

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