coe_J_smul

Mathlib.NumberTheory.ModularForms.Basic

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.coe_J_smul

English

The coe of J•τ equals −conj τ as a complex number.

Русский

Коэфицент J•τ равен −conj τ как комплексное число.

LaTeX

$$$\operatorname{coe}(J\cdot \tau) = -\overline{\tau}$$$

Lean4

theorem coe_J_smul (τ : ℍ) : (↑(J • τ) : ℂ) = -conj ↑τ := by
  simp [UpperHalfPlane.coe_smul, σ, J, show ¬(1 : ℝ) < 0 by simp, num, denom]

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

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

Разделы

Аффилиация

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