T

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

URI: https://scilib.ai/kg/mathlib#ModularGroup.T

English

The matrix T = [[1,1],[0,1]] represents a basic generator in SL(2,Z).

Русский

Матрица T = [[1,1],[0,1]] представляет базовый генератор в SL(2,Z).

LaTeX

$$↑T = !![1, 1; 0, 1]$$

Lean4

/-- The matrix `T = [[1, 1], [0, 1]]` as an element of `SL(2, ℤ)`. -/
def T : SL(2, ℤ) :=
  ⟨!![1, 1; 0, 1], by simp [Matrix.det_fin_two_of]⟩

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

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

Разделы

Аффилиация

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