im_T_smul

Mathlib.NumberTheory.Modular

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

English

The imaginary part remains unchanged after applying T: Im(T•z) = Im(z).

Русский

Мнимая часть не изменяется после применения T: Im(T•z) = Im(z).

LaTeX

$$$\\Im(T\\cdot z) = \\Im(z).$$$

Lean4

theorem im_T_smul : (T • z).im = z.im := by simpa using im_T_zpow_smul z 1

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

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

Разделы

Аффилиация

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