re_T_smul

Mathlib.NumberTheory.Modular

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

English

The real part after applying the basic translation T is increased by 1: Re(T•z) = Re(z) + 1.

Русский

Действие базового переноса T повышает вещественную часть на 1: Re(T•z) = Re(z) + 1.

LaTeX

$$$\\Re(T\\cdot z) = \\Re(z) + 1.$$$

Lean4

theorem re_T_smul : (T • z).re = z.re + 1 := by simpa using re_T_zpow_smul z 1

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

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

Разделы

Аффилиация

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