jacobiTheta₂'_add_right — Mathlib

English

Conjugation commutes with the derivative form: conj(θ₂'(z,τ)) = θ₂'(conj(z), -conj(τ)).

Русский

Сопряжение переставляет производную: conj(θ₂'(z,τ)) = θ₂'(conj(z), -conj(τ)).

LaTeX

$$$\overline{\theta_2'(z,\tau)} = \theta_2'(\overline{z}, -\overline{\tau})$$$

Lean4

theorem jacobiTheta₂'_add_right (z τ : ℂ) : jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ :=
  by
  refine tsum_congr (fun n ↦ ?_)
  simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, Complex.exp_add]
  suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]
  rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul, exp_two_pi_mul_I, one_zpow]

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