oddKernel_neg — Mathlib

English

For any a on the unit circle and x ∈ ℝ, oddKernel(−a, x) = −oddKernel(a, x).

Русский

Для любых a на единичной окружности и x ∈ ℝ выполняется oddKernel(−a, x) = −oddKernel(a, x).

LaTeX

$$$$\\text{oddKernel}(-a,x) = -\\text{oddKernel}(a,x).$$$$

Lean4

theorem oddKernel_neg (a : UnitAddCircle) (x : ℝ) : oddKernel (-a) x = -oddKernel a x := by
  induction a using QuotientAddGroup.induction_on with
  | H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, oddKernel_def, jacobiTheta₂''_neg_left]

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