T_inv_mul_apply_one

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

English

For g in SL(2, Z), (T^{-1} * g) acts on the singleton {1} the same as g acts on {1}.

Русский

Для g ∈ SL(2, Z) действие T^{-1} g на 1 совпадает с действием g на 1.

LaTeX

$$$ (T^{-1} \\cdot g) 1 = g 1 $$$

Lean4

@[simp]
theorem T_inv_mul_apply_one (g : SL(2, ℤ)) : (T⁻¹ * g) 1 = g 1 := by simpa using T_pow_mul_apply_one (-1) g

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

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

Разделы

Аффилиация

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