sinKernel_neg — Mathlib

English

For every a on the unit circle and every real x, the sine kernel is odd in its first argument: sinKernel(-a, x) = - sinKernel(a, x).

Русский

Для каждого a на единичном круге и любого действительного x син Kernel нечетна по первому аргументу: sinKernel(-a, x) = - sinKernel(a, x).

LaTeX

$$$\\sinKernel(-a, x) = -\\sinKernel(a, x). $$$

Lean4

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

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