SL_reduction_mod_hom_val

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

URI: https://scilib.ai/kg/mathlib#SL_reduction_mod_hom_val

English

The reduction modulo N map from SL(2, Z) to ZMod N sends each matrix entry to its residue mod N.

Русский

Редукция по модулю N из SL(2, Z) в ZMod N отправляет каждую отметку матрицы в её остаток по модулю N.

LaTeX

$$SLMOD(N) γ i j = (γ i j : ZMod N)$$

Lean4

@[simp]
theorem SL_reduction_mod_hom_val (γ : SL(2, ℤ)) (i j : Fin 2) : SLMOD(N) γ i j = (γ i j : ZMod N) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru