val_J

Mathlib.NumberTheory.ModularForms.Basic

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.val_J

English

The matrix J has the explicit representation with entries [[-1,0],[0,1]] in GL(2,ℝ).

Русский

Матрица J имеет явное представление в GL(2,ℝ) с элементами [[-1,0],[0,1]].

LaTeX

$$J.v a l = !![-1,0;0,1]$$

Lean4

@[simp]
theorem val_J : J.val = !![-1, 0; 0, 1] :=
  rfl

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

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

Разделы

Аффилиация

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