re_T_inv_smul

Mathlib.NumberTheory.Modular

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

English

The real part under T^{-1} decreases by 1: Re(T^{-1}•z) = Re(z) − 1.

Русский

При T^{-1} вещественная часть уменьшается на 1: Re(T^{-1}•z) = Re(z) − 1.

LaTeX

$$$\\Re(T^{-1}\\cdot z) = \\Re(z) - 1.$$$

Lean4

theorem re_T_inv_smul : (T⁻¹ • z).re = z.re - 1 := by simpa using re_T_zpow_smul z (-1)

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

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

Разделы

Аффилиация

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