coe_T_inv

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

English

The inverse of T, as an element of SL(2,Z), maps to the corresponding 2×2 integer matrix.

Русский

Обратная T в SL(2,Z) соответствует соответствующей целочисленной 2×2 матрице.

LaTeX

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

Lean4

theorem coe_T_inv : ↑(T⁻¹) = !![1, -1; 0, 1] := by simp [coe_inv, coe_T, adjugate_fin_two]

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

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

Разделы

Аффилиация

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