evenKernel_neg — Mathlib

English

cosKernel is even in a: cosKernel(-a, x) = cosKernel(a, x).

Русский

cosKernel не меняется при замене a на −a: cosKernel(−a, x) = cosKernel(a, x).

LaTeX

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

Lean4

@[simp]
theorem evenKernel_neg (a : UnitAddCircle) (x : ℝ) : evenKernel (-a) x = evenKernel a x := by
  induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]

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