jacobiTheta₂'_neg_left — Mathlib

English

Conjugation compatibility for θ₂': 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₂'_neg_left (z τ : ℂ) : jacobiTheta₂' (-z) τ = -jacobiTheta₂' z τ :=
  by
  rw [jacobiTheta₂', jacobiTheta₂', ← tsum_neg, ← (Equiv.neg ℤ).tsum_eq]
  congr 1 with n
  simp only [jacobiTheta₂'_term, jacobiTheta₂_term]
  rw [Equiv.neg_apply, ← neg_mul]
  push_cast
  ring_nf

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