oddKernel_undef — Mathlib

English

If a is an element of UnitAddCircle and x ≤ 0, then oddKernel(a) x = 0.

Русский

Если a ∈ UnitAddCircle и x ≤ 0, то oddKernel(a, x) = 0.

LaTeX

$$$$\\text{If } x \\le 0\\text{ then } \\text{oddKernel}(a,x) = 0. $$$$

Lean4

theorem oddKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : oddKernel a x = 0 := by
  induction a using QuotientAddGroup.induction_on with
  | H a' =>
    rw [← ofReal_eq_zero, oddKernel_def', jacobiTheta₂_undef, jacobiTheta₂'_undef, zero_div, zero_add, mul_zero,
        mul_zero] <;>
      simpa

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