cosZeta_neg_two_mul_nat_add_one — Mathlib

English

For any a on the unit circle and any natural number n, cosZeta(a)(-2(n+1)) = 0. These are trivial zeros on the negative even integers shifted by -2.

Русский

Для любого a на единичной окружности и любого натурального n, cosZeta(a)(-2(n+1)) = 0. Это тривиальные нули на отрицательных чётных целых числах со сдвигом -2.

LaTeX

$$$$\\cosZeta(a)(-2\\,(n+1)) = 0 \\quad(\\forall a, n).$$$$

Lean4

/-- The trivial zeroes of the cosine zeta function. -/
theorem cosZeta_neg_two_mul_nat_add_one (a : UnitAddCircle) (n : ℕ) : cosZeta a (-2 * (n + 1)) = 0 :=
  by
  have : (-2 : ℂ) * (n + 1) ≠ 0 := mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (Nat.cast_add_one_ne_zero n)
  rw [cosZeta, Function.update_of_ne this, Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by rw [neg_mul, Nat.cast_add_one]⟩, div_zero]

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