coe_T

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

English

The inverse of T has matrix [[1,-1],[0,1]] when viewed in the appropriate GL context.

Русский

Обратная T имеет матрицу [[1,-1],[0,1]] в соответствующем контексте GL.

LaTeX

$$↑(T⁻¹) = !![1, -1; 0, 1]$$

Lean4

theorem coe_T : ↑T = (!![1, 1; 0, 1] : Matrix _ _ ℤ) :=
  rfl

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

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

Разделы

Аффилиация

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